18 auto &body = f.second.body;
20 for(
auto it = body.instructions.begin(); it != body.instructions.end(); it++)
24 if(it->is_backwards_goto())
26 const auto &invariants =
static_cast<const exprt &
>(
27 it->condition().find(ID_C_spec_loop_invariant));
29 for(
const auto &invariant : invariants.operands())
33 source_location.set_comment(
"loop invariant");
38 body.insert_before_swap(it->get_target(), assertion);
Base class for all expressions.
const source_locationt & source_location() const
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void set_property_class(const irep_idt &property_class)
void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
Instrument Given Invariants.