CBMC
dfcc_loop_nesting_graph.cpp File Reference
+ Include dependency graph for dfcc_loop_nesting_graph.cpp:

Go to the source code of this file.

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...
 

Function Documentation

◆ build_loop_nesting_graph()

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.

Precondition
Loop normal form properties must hold.

Definition at line 27 of file dfcc_loop_nesting_graph.cpp.