20 std::vector<std::pair<goto_programt::targett, goto_programt::targett>>
spans;
28 for(
auto &loop : natural_loops.
loop_map)
30 auto head = loop.first;
31 auto &loop_instructions = loop.second;
33 if(loop_instructions.size() <= 1)
44 for(
const auto &t : loop_instructions)
46 if(t->is_goto() && t->get_target() == head)
50 log.error() <<
"Loop starting at:"
51 <<
"\n- head: " << head->source_location()
52 <<
"\nhas more than one latch instruction:"
53 <<
"\n- latch1: " << latch->source_location()
54 <<
"\n- latch2: " << t->source_location()
57 "Found loop with more than one latch instruction");
67 for(
const auto &span :
spans)
70 span.first->location_number <= head->location_number &&
71 head->location_number <= span.second->location_number;
74 span.first->location_number <= latch->location_number &&
75 latch->location_number <= span.second->location_number;
79 log.error() <<
"Loop spanning:"
80 <<
"\n- head: " << head->source_location()
81 <<
"\n- latch: " << latch->source_location()
82 <<
"\noverlaps loop spanning:"
83 <<
"\n- head: " << span.first->source_location()
84 <<
"\n- latch: " << span.second->source_location()
87 "Found loops with overlapping instruction spans");
91 spans.push_back({head, latch});
97 for(
const auto &i : loop_instructions)
100 i->location_number < head->location_number ||
101 i->location_number > latch->location_number)
103 log.error() <<
"Loop body instruction at:"
104 <<
"\n- " << i->source_location() <<
"\nis outside of"
105 <<
"\n- head: " << head->source_location()
106 <<
"\n- latch: " << latch->source_location()
109 "Found loop body instruction outside of the [head, latch] "
113 for(
const auto &
from : i->incoming_edges)
115 if(i != head && !loop_instructions.contains(
from))
117 log.error() <<
"Loop body instruction at:"
118 <<
"\n- " << i->source_location()
119 <<
"\n has incoming edge from outside the loop at:"
123 "Found loop body instruction with incoming edge from outside the "
138 "nested loop head and latch are in outer loop");
159 if(latch->has_condition() && !latch->condition().is_true())
200 latch->set_target(head);
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...