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.

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.

Definition at line 27 of file dfcc_loop_nesting_graph.cpp.