20 auto &body = f.second.body;
22 for(
auto it = body.instructions.begin(); it != body.instructions.end(); it++)
26 if(it->is_backwards_goto())
28 const auto &invariants =
static_cast<const exprt &
>(
30 if(!invariants.is_nil())
35 "Loop invariant is not side-effect free.",
36 it->condition().find_source_location());
40 for(
const auto &invariant : invariants.operands())
42 auto source_location = invariant.source_location();
43 source_location.set_property_class(
"invariant");
44 source_location.set_comment(
"loop invariant");
49 body.insert_before_swap(it->get_target(), assertion);