CBMC
cover_basic_blockst::block_infot Struct Reference
+ Collaboration diagram for cover_basic_blockst::block_infot:

Public Attributes

std::optional< goto_programt::const_targettrepresentative_inst
 the program location to instrument for this block More...
 
source_locationt source_location
 the source location representative for this block (we need a separate copy of source locations because we attach the line number ranges to them) More...
 
source_linest source_lines
 the set of source code lines belonging to this block More...
 

Detailed Description

Definition at line 110 of file cover_basic_blocks.h.

Member Data Documentation

◆ representative_inst

std::optional<goto_programt::const_targett> cover_basic_blockst::block_infot::representative_inst

the program location to instrument for this block

Definition at line 113 of file cover_basic_blocks.h.

◆ source_lines

source_linest cover_basic_blockst::block_infot::source_lines

the set of source code lines belonging to this block

Definition at line 121 of file cover_basic_blocks.h.

◆ source_location

source_locationt cover_basic_blockst::block_infot::source_location

the source location representative for this block (we need a separate copy of source locations because we attach the line number ranges to them)

Definition at line 118 of file cover_basic_blocks.h.


The documentation for this struct was generated from the following file: