20 #ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H
21 #define CPROVER_ANALYSES_NATURAL_LOOPS_H
46 template <
class P,
class T>
85 goto_programt::const_targett>
94 show_loops<natural_loopst>(goto_model, out);
102 template<
class P,
class T>
105 cfg_dominators(program);
108 cfg_dominators.output(std::cout);
112 for(T m_it=program.instructions.begin();
113 m_it!=program.instructions.end();
116 if(m_it->is_backwards_goto())
118 const auto &target=m_it->get_target();
120 if(target->location_number<=m_it->location_number)
123 std::cout <<
"Computing loop for "
124 << m_it->location_number <<
" -> "
125 << target->location_number <<
"\n";
128 if(cfg_dominators.dominates(target, m_it))
129 compute_natural_loop(m_it, target);
136 template<
class P,
class T>
139 assert(n->location_number<=m->location_number);
143 auto insert_result = parentt::loop_map.emplace(n,
natural_loopt{});
158 while(!stack.empty())
163 const nodet &node = cfg_dominators.get_node(p);
165 for(
const auto &edge : node.in)
167 T q=cfg_dominators.cfg[edge.first].PC;
Compute dominators for CFG of goto_function.
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(P &program)
void operator()(P &program)
natural_loops_templatet()
void compute_natural_loop(T, T)
Computes the natural loop for a given back-edge (see Muchnick section 7.4)
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
cfg_dominators_templatet< P, T, false > cfg_dominators
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
void compute(P &program)
Finds all back-edges and computes the natural loops.
parentt::loopt natural_loopt
loop_analysist< T > parentt
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 > natural_loops_mutablet
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)