CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp File Reference

CBMC

Loading...

Searching...

No Matches

dfcc_loop_nesting_graph.cpp File Reference

#include "dfcc_loop_nesting_graph.h"
#include <analyses/natural_loops.h>

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