22 : head(head), latch(latch), instructions(instructions)
32 for(
auto &loop : natural_loops.
loop_map)
35 auto &loop_instructions = loop.second;
37 if(loop_instructions.size() <= 1)
47 for(
const auto &t : loop_instructions)
50 t->is_goto() && t->get_target() ==
loop_head &&
51 t->location_number >
loop_latch->location_number)
82 "loop_nesting_graph must be acyclic");
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
Builds a graph instance describing the nesting structure of natural loops in the given goto_program.
Builds a graph describing how loops are nested in a GOTO program.
Compute natural loops in a goto_function.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
dfcc_loop_nesting_graph_nodet(const goto_programt::targett &head, const goto_programt::targett &latch, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &instructions)