37#ifndef CPROVER_ANALYSES_LEXICAL_LOOPS_H
38#define CPROVER_ANALYSES_LEXICAL_LOOPS_H
63template <
class P,
class T>
92 out <<
"Note not all loops were in lexical loop form\n";
114template <
class P,
class T>
117 all_in_lexical_loop_form =
true;
120 for(
auto it = program.instructions.begin(); it != program.instructions.end();
123 if(it->is_backwards_goto())
125 const auto &target = it->get_target();
127 if(target->location_number <= it->location_number)
130 std::cout <<
"Computing loop for " << it->location_number <<
" -> "
131 << target->location_number <<
"\n";
134 if(!compute_lexical_loop(it, target))
135 all_in_lexical_loop_form =
false;
145template <
class P,
class T>
152 "loop header should come lexically before the tail");
155 std::set<T> loop_instructions;
163 while(!stack.empty())
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::const_iterator const_targett
Main driver for working out if a class (normally goto_programt) has any lexical loops.
loop_analysist< T > parentt
lexical_loops_templatet(P &program)
bool all_cycles_in_lexical_loop_form() const
bool all_in_lexical_loop_form
virtual ~lexical_loops_templatet()=default
bool compute_lexical_loop(T, T)
Computes the lexical loop for a given back-edge by walking backwards from the tail,...
void operator()(P &program)
void compute(P &program)
Finds all back-edges and computes the lexical loops.
void output(std::ostream &out) const
Print all natural loops that were found.
parentt::loopt lexical_loopt
lexical_loops_templatet()=default
virtual void output(std::ostream &) const
Print all natural loops that were found.
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
lexical_loops_templatet< const goto_programt, goto_programt::const_targett > lexical_loopst
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.