CBMC
lexical_loops_templatet< P, T, C > Class Template Reference

Main driver for working out if a class (normally goto_programt) has any lexical loops. More...

#include <lexical_loops.h>

+ Inheritance diagram for lexical_loops_templatet< P, T, C >:
+ Collaboration diagram for lexical_loops_templatet< P, T, C >:

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
 

Detailed Description

template<class P, class T, typename C>
class lexical_loops_templatet< P, T, C >

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.

Template Parameters
Pthe program representation and needs:
  • [field] instruction which is an iterable of type T.
Titerator of the particular node type, e.g. std::list<...>::iterator. The object this iterator holds needs:
  • [function] is_backwards_goto() returning a bool.
  • [function] get_target() which returns an object that needs:
    • [field] location_number which is an unsigned int.
Ccomparison to use over T typed elements

Definition at line 65 of file lexical_loops.h.

Member Typedef Documentation

◆ lexical_loopt

template<class P , class T , typename C >
typedef parentt::loopt lexical_loops_templatet< P, T, C >::lexical_loopt

Definition at line 70 of file lexical_loops.h.

◆ parentt

template<class P , class T , typename C >
typedef loop_analysist<T, C> lexical_loops_templatet< P, T, C >::parentt
private

Definition at line 67 of file lexical_loops.h.

Constructor & Destructor Documentation

◆ lexical_loops_templatet() [1/2]

template<class P , class T , typename C >
lexical_loops_templatet< P, T, C >::lexical_loops_templatet ( )
default

◆ lexical_loops_templatet() [2/2]

template<class P , class T , typename C >
lexical_loops_templatet< P, T, C >::lexical_loops_templatet ( P &  program)
inlineexplicit

Definition at line 79 of file lexical_loops.h.

◆ ~lexical_loops_templatet()

template<class P , class T , typename C >
virtual lexical_loops_templatet< P, T, C >::~lexical_loops_templatet ( )
virtualdefault

Member Function Documentation

◆ all_cycles_in_lexical_loop_form()

template<class P , class T , typename C >
bool lexical_loops_templatet< P, T, C >::all_cycles_in_lexical_loop_form ( ) const
inline

Definition at line 84 of file lexical_loops.h.

◆ compute()

template<class P , class T , typename C >
void lexical_loops_templatet< P, T, C >::compute ( P &  program)
protected

Finds all back-edges and computes the lexical loops.

Definition at line 117 of file lexical_loops.h.

◆ compute_lexical_loop()

template<class P , class T , typename C >
bool lexical_loops_templatet< P, T, C >::compute_lexical_loop ( loop_tail,
loop_head 
)
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.

◆ operator()()

template<class P , class T , typename C >
void lexical_loops_templatet< P, T, C >::operator() ( P &  program)
inline

Definition at line 72 of file lexical_loops.h.

◆ output()

template<class P , class T , typename C >
void lexical_loops_templatet< P, T, C >::output ( std::ostream &  out) const
inlinevirtual

Print all natural loops that were found.

Reimplemented from loop_analysist< T, C >.

Definition at line 89 of file lexical_loops.h.

Member Data Documentation

◆ all_in_lexical_loop_form

template<class P , class T , typename C >
bool lexical_loops_templatet< P, T, C >::all_in_lexical_loop_form = false
protected

Definition at line 102 of file lexical_loops.h.


The documentation for this class was generated from the following file: