CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
scope_tree.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: Scope Tree
4
5 Author: John Dumbell, john.dumbell@diffblue.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
10#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
11
12#include <util/graph.h>
13#include <util/std_code_base.h>
14
16
17#include <unordered_set>
18
19typedef std::size_t node_indext;
20
46
50{
51public:
53 : destructor(code), node_id(id)
54 {
55 }
56
59};
60
93{
94public:
96 {
111 std::unordered_set<irep_idt, irep_id_hash> accounted_flags;
112 };
113
115 {
116 // We add a default node to the graph to act as a root for path traversal.
117 this->scope_graph.add_node();
118 }
119
124 void add(
125 const codet &destructor,
126 std::optional<goto_programt::targett> declaration);
127
129 std::optional<codet> &get_destructor(node_indext index);
130
132 std::optional<declaration_statet> &get_declaration(node_indext index);
133
142 const std::vector<destructor_and_idt> get_destructors(
143 std::optional<node_indext> end_index = {},
144 std::optional<node_indext> starting_index = {});
145
152
156 void set_current_node(std::optional<node_indext> val);
157
161
164
166 void descend_tree();
167
169 void output_dot(std::ostream &os) const
170 {
171 scope_graph.output_dot(os);
172 }
173
174private:
175 class scope_nodet : public graph_nodet<empty_edget>
176 {
177 public:
178 scope_nodet() = default;
179
180 explicit scope_nodet(
181 codet destructor,
182 std::optional<declaration_statet> declaration);
183
184 std::optional<codet> destructor_value;
185 std::optional<declaration_statet> declaration;
186
187 std::string dot_attributes(const node_indext &n) const override
188 {
189 if(!declaration.has_value())
190 return "";
191
192 return id2string(
193 declaration->instruction->decl_symbol().get_identifier());
194 }
195 };
196
199};
200
201#endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Result of an attempt to find ancestor information about two nodes.
Definition scope_tree.h:25
std::size_t left_depth_below_common_ancestor
Definition scope_tree.h:43
ancestry_resultt(node_indext node)
Definition scope_tree.h:27
std::size_t right_depth_below_common_ancestor
Definition scope_tree.h:44
node_indext common_ancestor
Definition scope_tree.h:42
ancestry_resultt(node_indext node, std::size_t left_pre_size, std::size_t right_pre_size)
Definition scope_tree.h:33
Data structure for representing an arbitrary statement in a program.
Result of a tree query holding both destructor codet and the ID of the node that held it.
Definition scope_tree.h:50
node_indext node_id
Definition scope_tree.h:58
const codet destructor
Definition scope_tree.h:57
destructor_and_idt(const codet &code, node_indext id)
Definition scope_tree.h:52
instructionst::iterator targett
This class represents a node in a directed graph.
Definition graph.h:35
std::size_t node_indext
Definition graph.h:37
std::optional< codet > destructor_value
Definition scope_tree.h:184
std::optional< declaration_statet > declaration
Definition scope_tree.h:185
std::string dot_attributes(const node_indext &n) const override
Node with attributes suitable for Graphviz DOT format.
Definition scope_tree.h:187
Tree to keep track of the destructors generated along each branch of a function.
Definition scope_tree.h:93
node_indext current_node
Definition scope_tree.h:198
grapht< scope_nodet > scope_graph
Definition scope_tree.h:197
std::optional< declaration_statet > & get_declaration(node_indext index)
Fetches the declaration value for the passed-in node index.
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
void output_dot(std::ostream &os) const
Output scope tree to os in dot format.
Definition scope_tree.h:169
void descend_tree()
Walks the current node down to its child.
void set_current_node(std::optional< node_indext > val)
Sets the current node.
const std::vector< destructor_and_idt > get_destructors(std::optional< node_indext > end_index={}, std::optional< node_indext > starting_index={})
Builds a vector of destructors that start from starting_index and ends at end_index.
std::optional< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
Concrete Goto Program.
A Template Class for Graphs.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::size_t node_indext
Definition scope_tree.h:19
std::unordered_set< irep_idt, irep_id_hash > accounted_flags
In order to handle user goto statements which jump into a scope the declaration may need to be follow...
Definition scope_tree.h:111
goto_programt::targett instruction
This is an iterator which points to the instruction where the declaration takes place.
Definition scope_tree.h:99