CBMC
dfcc_loop_nesting_graph.h File Reference

Builds a graph describing how loops are nested in a GOTO program. More...

#include <util/graph.h>
#include <analyses/loop_analysis.h>
+ Include dependency graph for dfcc_loop_nesting_graph.h:
+ This graph shows which files directly or indirectly include this file:

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

Detailed Description

Builds a graph describing how loops are nested in a GOTO program.

Definition in file dfcc_loop_nesting_graph.h.

Typedef Documentation

◆ dfcc_loop_nesting_grapht

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.

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.

Precondition
Loop normal form properties must hold.

Definition at line 27 of file dfcc_loop_nesting_graph.cpp.