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);