16#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_NESTING_GRAPH_H
17#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_NESTING_GRAPH_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
This class represents a node in a directed graph.
A loop, specified as a set of instructions.
Class that provides messages with a built-in verbosity 'level'.
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.
grapht< dfcc_loop_nesting_graph_nodet > dfcc_loop_nesting_grapht
A Template Class for Graphs.
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...
A graph node that stores information about a natural loop.
loop_templatet< goto_programt::targett, goto_programt::target_less_than > instructions
Set of loop instructions.
goto_programt::targett head
Loop head instruction.
goto_programt::targett latch
Loop latch instruction.
A total order over targett and const_targett.
1.9.8 
