CBMC
|
Builds a graph describing how loops are nested in a GOTO program. More...
Go to the source code of this file.
Classes | |
struct | dfcc_loop_nesting_graph_nodet |
A graph node that stores information about a natural loop. More... | |
Typedefs | |
typedef grapht< dfcc_loop_nesting_graph_nodet > | dfcc_loop_nesting_grapht |
Functions | |
dfcc_loop_nesting_grapht | build_loop_nesting_graph (goto_programt &goto_program) |
Builds a graph instance describing the nesting structure of natural loops in the given goto_program . More... | |
Builds a graph describing how loops are nested in a GOTO program.
Definition in file dfcc_loop_nesting_graph.h.
Definition at line 47 of file dfcc_loop_nesting_graph.h.
dfcc_loop_nesting_grapht build_loop_nesting_graph | ( | goto_programt & | goto_program | ) |
Builds a graph instance describing the nesting structure of natural loops in the given goto_program
.
A loop is considered nested in an outer loop if its head and its latch are both found in the instructions of the outer loop.
Definition at line 27 of file dfcc_loop_nesting_graph.cpp.