cprover
|
#include <natural_loops.h>
Public Types | |
typedef std::set< T > | natural_loopt |
typedef std::map< T, natural_loopt > | loop_mapt |
Public Member Functions | |
void | operator() (P &program) |
void | output (std::ostream &) const |
Print all natural loops that were found. More... | |
const cfg_dominators_templatet< P, T, false > & | get_dominator_info () const |
natural_loops_templatet () | |
natural_loops_templatet (P &program) | |
Public Attributes | |
loop_mapt | loop_map |
Protected Types | |
typedef cfg_dominators_templatet< P, T, false >::cfgt::nodet | nodet |
Protected Member Functions | |
void | compute (P &program) |
Finds all back-edges and computes the natural loops. More... | |
void | compute_natural_loop (T, T) |
Computes the natural loop for a given back-edge (see Muchnick section 7.4) More... | |
Protected Attributes | |
cfg_dominators_templatet< P, T, false > | cfg_dominators |
Definition at line 24 of file natural_loops.h.
typedef std::map<T, natural_loopt> natural_loops_templatet< P, T >::loop_mapt |
Definition at line 30 of file natural_loops.h.
typedef std::set<T> natural_loops_templatet< P, T >::natural_loopt |
Definition at line 27 of file natural_loops.h.
|
protected |
Definition at line 57 of file natural_loops.h.
|
inline |
Definition at line 46 of file natural_loops.h.
|
inlineexplicit |
Definition at line 50 of file natural_loops.h.
|
protected |
Finds all back-edges and computes the natural loops.
Definition at line 82 of file natural_loops.h.
Referenced by natural_loops_templatet< const goto_programt, goto_programt::const_targett >::natural_loops_templatet(), and natural_loops_templatet< const goto_programt, goto_programt::const_targett >::operator()().
|
protected |
Computes the natural loop for a given back-edge (see Muchnick section 7.4)
Definition at line 119 of file natural_loops.h.
|
inline |
Definition at line 41 of file natural_loops.h.
Referenced by goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_goto(), and goto_program2codet::convert_goto_switch().
|
inline |
Definition at line 34 of file natural_loops.h.
void natural_loops_templatet< P, T >::output | ( | std::ostream & | out | ) | const |
Print all natural loops that were found.
Definition at line 154 of file natural_loops.h.
Referenced by show_natural_loops().
|
protected |
Definition at line 56 of file natural_loops.h.
Referenced by natural_loops_templatet< const goto_programt, goto_programt::const_targett >::get_dominator_info().
loop_mapt natural_loops_templatet< P, T >::loop_map |
Definition at line 32 of file natural_loops.h.
Referenced by acceleratet::accelerate_loop(), acceleratet::accelerate_loops(), goto_program2codet::build_loop_map(), code_contractst::code_contracts(), acceleratet::contains_nested_loops(), acceleratet::find_back_jump(), havoc_loopst::havoc_loops(), k_inductiont::k_induction(), and acceleratet::make_overflow_loc().