CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_loop_nesting_graph.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Qinheping Hu, qinhh@amazon.com
6
7Author: Remi Delmas, delmasrd@amazon.com
8
9Date: March 2023
10
11\*******************************************************************/
12
15
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
18
19#include <util/graph.h>
20
22
23class messaget;
24
46
48
54
55#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
This class represents a node in a directed graph.
Definition graph.h:35
A loop, specified as a set of instructions.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
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.