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

P	the program representation and needs: [field] instruction which is an iterable of type T.
T	iterator 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.
C	comparison 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 ( T  loop_tail, T  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:

• /home/runner/work/cbmc/cbmc/src/analyses/lexical_loops.h