20#ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H
21#define CPROVER_ANALYSES_NATURAL_LOOPS_H
46template <
class P,
class T>
85 goto_programt::const_targett>
102template<
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);
136template<
class P,
class T>
139 assert(
n->location_number<=m->location_number);
152 loop.insert_instruction(
n);
153 loop.insert_instruction(m);
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;
168 if(loop.insert_instruction(
q))
Compute dominators for CFG of goto_function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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)
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
cfg_dominators_templatet< P, T, false > cfg_dominators
void compute(P &program)
Finds all back-edges and computes the natural loops.
parentt::loopt natural_loopt
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
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)