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

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

typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht

Definition at line 47 of file dfcc_loop_nesting_graph.h.

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.