20 #ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H
21 #define CPROVER_ANALYSES_NATURAL_LOOPS_H
47 template <
class P,
class T,
typename C>
86 goto_programt::const_targett,
87 goto_programt::target_less_than>
99 show_loops<natural_loopst>(goto_model, out);
107 template <
class P,
class T,
typename C>
110 cfg_dominators(program);
113 cfg_dominators.output(std::cout);
117 for(T m_it=program.instructions.begin();
118 m_it!=program.instructions.end();
121 if(m_it->is_backwards_goto())
123 const auto &target=m_it->get_target();
125 if(target->location_number<=m_it->location_number)
128 std::cout <<
"Computing loop for "
129 << m_it->location_number <<
" -> "
130 << target->location_number <<
"\n";
133 if(cfg_dominators.dominates(target, m_it))
134 compute_natural_loop(m_it, target);
141 template <
class P,
class T,
typename C>
148 auto insert_result = parentt::loop_map.emplace(n,
natural_loopt{});
163 while(!stack.empty())
168 const nodet &node = cfg_dominators.get_node(p);
170 for(
const auto &edge : node.in)
172 T q=cfg_dominators.cfg[edge.first].PC;
Compute dominators for CFG of goto_function.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
A loop, specified as a set of instructions.
bool insert_instruction(const T instruction)
Adds instruction to this loop.
Main driver for working out if a class (normally goto_programt) has any natural loops.
natural_loops_templatet()
cfg_dominators_templatet< P, T, false > cfg_dominators
void operator()(P &program)
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
parentt::loopt natural_loopt
void compute_natural_loop(T, T)
Computes the natural loop for a given back-edge (see Muchnick section 7.4)
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
loop_analysist< T, C > parentt
void compute(P &program)
Finds all back-edges and computes the natural loops.
natural_loops_templatet(P &program)
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...
natural_loops_templatet< goto_programt, goto_programt::targett, goto_programt::target_less_than > natural_loops_mutablet
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
#define PRECONDITION(CONDITION)
A total order over targett and const_targett.