31 auto &instruction = *it;
32 std::vector<goto_programt::targett> backedges;
37 for(
auto predecessor : instruction.incoming_edges)
39 if(predecessor->location_number > instruction.location_number)
40 backedges.push_back(predecessor);
43 if(backedges.size() < 2)
48 auto last_backedge = backedges.back();
53 if(!last_backedge->is_goto() || last_backedge->targets.size() > 1)
60 if(!last_backedge->condition().is_true())
66 last_backedge->condition_nonconst() =
not_exprt(last_backedge->condition());
67 last_backedge->set_target(std::next(new_goto));
69 last_backedge = new_goto;
78 for(
auto backedge : backedges)
80 if(backedge->is_goto() && backedge->targets.size() == 1)
82 backedge->set_target(last_backedge);
105 natural_loops{goto_program};
106 std::set<goto_programt::targett, location_number_less_thant> modified_loops;
108 for(
auto it1 = natural_loops.loop_map.begin();
109 it1 != natural_loops.loop_map.end();
112 DATA_INVARIANT(!it1->second.empty(),
"loops cannot have no instructions");
115 (*std::prev(it1->second.end()))->is_goto() &&
116 (*std::prev(it1->second.end()))->get_target() == it1->first)
118 if(modified_loops.find(it1->first) != modified_loops.end())
122 for(
auto it2 = natural_loops.loop_map.begin();
123 it2 != natural_loops.loop_map.end();
140 modified_loops.find(it2->first) == modified_loops.end() &&
141 (!(*std::prev(it2->second.end()))->is_goto() ||
142 (*std::prev(it2->second.end()))->get_target() != it2->first))
145 *std::prev(it2->second.end()),
147 it2->first, (*std::prev(it2->second.end()))->source_location()));
148 it2->second.insert_instruction(new_goto);
149 it1->second.insert_instruction(new_goto);
150 modified_loops.insert(it2->first);
154 *std::prev(it1->second.end()),
156 it1->first, (*std::prev(it1->second.end()))->source_location()));
157 modified_loops.insert(it1->first);
163 if(!modified_loops.empty())
166 bool any_change = !modified_loops.empty();
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...