22 return a->location_number < b->location_number;
29 auto &instruction = *it;
30 std::vector<goto_programt::targett> backedges;
35 for(
auto predecessor : instruction.incoming_edges)
37 if(predecessor->location_number > instruction.location_number)
38 backedges.push_back(predecessor);
41 if(backedges.size() < 2)
46 auto last_backedge = backedges.back();
51 if(!last_backedge->is_goto() || last_backedge->targets.size() > 1)
58 if(!last_backedge->guard.is_true())
64 last_backedge->guard =
not_exprt(last_backedge->guard);
65 last_backedge->set_target(std::next(new_goto));
67 last_backedge = new_goto;
76 for(
auto backedge : backedges)
78 if(backedge->is_goto() && backedge->targets.size() == 1)
80 backedge->set_target(last_backedge);
89 bool any_change =
false;
107 goto_function.body.update();
117 bool any_change =
false;
function_mapt function_map
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
void compute_location_numbers()
Re-number our goto_function.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static bool location_number_less_than(const goto_programt::targett &a, const goto_programt::targett &b)
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Ensure one backedge per target.