25 const std::size_t block_nr = basic_blocks.
block_of(i_it);
26 const auto representative_instruction = basic_blocks.
instruction_of(block_nr);
28 if(representative_instruction && *representative_instruction == i_it)
31 const std::string
id =
id2string(i_it->function) +
"#" + b;
37 const std::string
comment =
"block " + b;
38 const irep_idt function = i_it->function;
41 i_it->source_location = source_location;
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::string comment(const rw_set_baset::entryt &entry, bool write)
Coverage Instrumentation.
Basic blocks detection for Coverage Instrumentation.
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
instructionst::iterator targett
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
virtual std::size_t block_of(goto_programt::const_targett t) const =0
The boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const goal_filterst & goal_filters
Filters for the Coverage Instrumentation.
goto_programt & goto_program
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function) const
bool is_non_cover_assertion(goto_programt::const_targett t) const
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0