cprover
Loading...
Searching...
No Matches
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.

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.