39 i_it,
id2string(i_it->source_location.get_comment()), i_it->function);
49 if(i_it->is_function_call())
54 code_function_call.
function().
id() == ID_symbol &&
57 code_function_call.
arguments().size() == 1)
61 "condition `" +
from_expr(
ns, i_it->function, c) +
"'";
77 while(!if_it->is_function_call())
81 "additional goal to ensure reachability of end of function";
84 if_it->source_location.set_comment(
comment);
85 if_it->source_location.set_property_class(
"reachability_constraint");
86 if_it->source_location.set_function(
function);
87 if_it->function =
function;
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)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void cover_instrument_end_of_function(const irep_idt &function, goto_programt &goto_program)
Coverage Instrumentation.
const irep_idt & id() const
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Coverage Instrumentation Utilities.
The boolean constant false.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
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.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Base class for all expressions.
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
const code_function_callt & to_code_function_call(const codet &code)