CBMC
dfcc_loop_nesting_graph.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 
7 Author: Remi Delmas, delmasrd@amazon.com
8 
9 Date: 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 
21 #include <analyses/loop_analysis.h>
22 
23 class messaget;
24 
26 struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
27 {
28 public:
29  dfcc_loop_nesting_graph_nodet(
30  const goto_programt::targett &head,
31  const goto_programt::targett &latch,
32  const loop_templatet<
33  goto_programt::targett,
34  goto_programt::target_less_than> &instructions);
35 
37  goto_programt::targett head;
38 
40  goto_programt::targett latch;
41 
43  loop_templatet<goto_programt::targett, goto_programt::target_less_than>
44  instructions;
45 };
46 
47 typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
48 
53 dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program);
54 
55 #endif
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:614
graph_nodet
This class represents a node in a directed graph.
Definition: graph.h:35
grapht
A generic directed graph with a parametric node type.
Definition: graph.h:167
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
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.
Definition: dfcc_loop_nesting_graph.cpp:27
dfcc_loop_nesting_grapht
grapht< dfcc_loop_nesting_graph_nodet > dfcc_loop_nesting_grapht
Definition: dfcc_loop_nesting_graph.h:47
graph.h
A Template Class for Graphs.
loop_analysis.h
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...
dfcc_loop_nesting_graph_nodet
A graph node that stores information about a natural loop.
Definition: dfcc_loop_nesting_graph.h:27
dfcc_loop_nesting_graph_nodet::instructions
loop_templatet< goto_programt::targett, goto_programt::target_less_than > instructions
Set of loop instructions.
Definition: dfcc_loop_nesting_graph.h:44
dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet
dfcc_loop_nesting_graph_nodet(const goto_programt::targett &head, const goto_programt::targett &latch, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &instructions)
Definition: dfcc_loop_nesting_graph.cpp:17
dfcc_loop_nesting_graph_nodet::head
goto_programt::targett head
Loop head instruction.
Definition: dfcc_loop_nesting_graph.h:37
dfcc_loop_nesting_graph_nodet::latch
goto_programt::targett latch
Loop latch instruction.
Definition: dfcc_loop_nesting_graph.h:40
goto_programt::instructiont::target_less_than
A total order over targett and const_targett.
Definition: goto_program.h:392