Go to the documentation of this file.
25 i_it->turn_into_skip();
41 i_it,
id2string(i_it->source_location.get_comment()), function_id);
52 if(i_it->is_function_call())
57 code_function_call.
function().
id() == ID_symbol &&
60 code_function_call.
arguments().size() == 1)
71 i_it->turn_into_skip();
78 const auto last_function_call = std::find_if(
82 return instruction.is_function_call();
86 "Goto program should have at least one function call");
88 last_function_call != goto_program.
instructions.rbegin(),
89 "Goto program shouldn't end with a function call");
90 const auto if_it = last_function_call.base();
92 "additional goal to ensure reachability of end of function";
95 if_it->source_location.set_comment(
comment);
96 if_it->source_location.set_property_class(
"reachability_constraint");
97 if_it->source_location.set_function(function_id);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool is_non_cover_assertion(goto_programt::const_targett t) const
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
Base class for all expressions.
codet representation of a function call statement.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const std::string & id2string(const irep_idt &d)
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program)
const irep_idt & get_identifier() const
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
The Boolean constant false.
instructionst instructions
The list of instructions in the goto program.
void instrument(const irep_idt &function_id, 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(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
static std::string comment(const rw_set_baset::entryt &entry, bool write)
This class represents an instruction in the GOTO intermediate representation.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
instructionst::iterator targett