37#ifndef CPROVER_ANALYSES_LEXICAL_LOOPS_H
38#define CPROVER_ANALYSES_LEXICAL_LOOPS_H
64template <
class P,
class T,
typename C>
93 out <<
"Note not all loops were in lexical loop form\n";
116template <
class P,
class T,
typename C>
119 all_in_lexical_loop_form =
true;
122 for(
auto it = program.instructions.begin(); it != program.instructions.end();
125 if(it->is_backwards_goto())
127 const auto &target = it->get_target();
129 if(target->location_number <= it->location_number)
132 std::cout <<
"Computing loop for " << it->location_number <<
" -> "
133 << target->location_number <<
"\n";
136 if(!compute_lexical_loop(it, target))
137 all_in_lexical_loop_form =
false;
147template <
class P,
class T,
typename C>
154 "loop header should come lexically before the tail");
157 std::set<T, C> loop_instructions;
165 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.
bool all_in_lexical_loop_form
lexical_loops_templatet(P &program)
loop_analysist< T, C > parentt
lexical_loops_templatet()=default
bool all_cycles_in_lexical_loop_form() const
bool compute_lexical_loop(T, T)
Computes the lexical loop for a given back-edge by walking backwards from the tail,...
virtual ~lexical_loops_templatet()=default
void compute(P &program)
Finds all back-edges and computes the lexical loops.
void operator()(P &program)
parentt::loopt lexical_loopt
void output(std::ostream &out) const
Print all natural loops that were found.
virtual void output(std::ostream &) const
Print all natural loops that were found.
lexical_loops_templatet< const goto_programt, goto_programt::const_targett, goto_programt::target_less_than > lexical_loopst
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
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'.
A total order over targett and const_targett.