CBMC
|
Main driver for working out if a class (normally goto_programt) has any lexical loops. More...
#include <lexical_loops.h>
Public Types | |
typedef parentt::loopt | lexical_loopt |
Public Types inherited from loop_analysist< T, C > | |
typedef loop_templatet< T, C > | loopt |
typedef std::map< T, loopt, C > | loop_mapt |
Public Member Functions | |
void | operator() (P &program) |
lexical_loops_templatet ()=default | |
lexical_loops_templatet (P &program) | |
bool | all_cycles_in_lexical_loop_form () const |
void | output (std::ostream &out) const |
Print all natural loops that were found. More... | |
virtual | ~lexical_loops_templatet ()=default |
Public Member Functions inherited from loop_analysist< T, C > | |
bool | is_loop_header (const T instruction) const |
Returns true if instruction is the header of any loop. More... | |
loop_analysist ()=default | |
Protected Member Functions | |
void | compute (P &program) |
Finds all back-edges and computes the lexical loops. More... | |
bool | compute_lexical_loop (T, T) |
Computes the lexical loop for a given back-edge by walking backwards from the tail, abandoning the candidate loop if we stray outside the bounds of the lexical region bounded by the head and tail, otherwise recording all instructions that can reach the backedge as falling within the loop. More... | |
Protected Attributes | |
bool | all_in_lexical_loop_form = false |
Private Types | |
typedef loop_analysist< T, C > | parentt |
Additional Inherited Members | |
Public Attributes inherited from loop_analysist< T, C > | |
loop_mapt | loop_map |
Main driver for working out if a class (normally goto_programt) has any lexical loops.
compute takes an entire goto_programt, iterates over the instructions and for any backwards jumps attempts to find out if it's a lexical loop.
All instructions in a lexical loop are stored into loop_map, keyed by their head - the target of the backwards goto jump.
P | the program representation and needs:
|
T | iterator of the particular node type, e.g. std::list<...>::iterator. The object this iterator holds needs:
|
C | comparison to use over T typed elements |
Definition at line 65 of file lexical_loops.h.
typedef parentt::loopt lexical_loops_templatet< P, T, C >::lexical_loopt |
Definition at line 70 of file lexical_loops.h.
|
private |
Definition at line 67 of file lexical_loops.h.
|
default |
|
inlineexplicit |
Definition at line 79 of file lexical_loops.h.
|
virtualdefault |
|
inline |
Definition at line 84 of file lexical_loops.h.
|
protected |
Finds all back-edges and computes the lexical loops.
Definition at line 117 of file lexical_loops.h.
|
protected |
Computes the lexical loop for a given back-edge by walking backwards from the tail, abandoning the candidate loop if we stray outside the bounds of the lexical region bounded by the head and tail, otherwise recording all instructions that can reach the backedge as falling within the loop.
Definition at line 148 of file lexical_loops.h.
|
inline |
Definition at line 72 of file lexical_loops.h.
|
inlinevirtual |
Print all natural loops that were found.
Reimplemented from loop_analysist< T, C >.
Definition at line 89 of file lexical_loops.h.
|
protected |
Definition at line 102 of file lexical_loops.h.