CBMC
Loading...
Searching...
No Matches
scope_tree.cpp
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#include "scope_tree.h"
10
12 const codet &destructor,
13 std::optional<goto_programt::targett> declaration)
14{
16 using declaration_optt = std::optional<declaration_statet>;
17 auto declaration_opt =
18 declaration ? declaration_optt{{*declaration}} : declaration_optt{};
19 auto new_node = scope_graph.add_node(destructor, std::move(declaration_opt));
22}
23
24std::optional<codet> &scope_treet::get_destructor(node_indext index)
25{
26 PRECONDITION(index < scope_graph.size());
27 return scope_graph[index].destructor_value;
28}
29
30std::optional<scope_treet::declaration_statet> &
32{
33 PRECONDITION(index < scope_graph.size());
34 return scope_graph[index].declaration;
35}
36
40{
41 std::size_t left_unique_count = 0, right_unique_count = 0;
42 while(right_index != left_index)
43 {
45 {
48 !edge_map.empty(),
49 "Node at index " + std::to_string(right_index) +
50 " has no parent, can't find an ancestor.");
51 right_index = edge_map.begin()->first, right_unique_count++;
52 }
53 else
54 {
57 !edge_map.empty(),
58 "Node at index " + std::to_string(left_index) +
59 " has no parent, can't find an ancestor.");
60 left_index = edge_map.begin()->first, left_unique_count++;
61 }
62 }
63
64 // At this point it doesn't matter which index we return as both are the same.
66}
67
68const std::vector<destructor_and_idt> scope_treet::get_destructors(
69 std::optional<node_indext> end_index,
70 std::optional<node_indext> starting_index)
71{
72 node_indext next_id = starting_index.value_or(get_current_node());
73 node_indext end_id = end_index.value_or(0);
74
75 std::vector<destructor_and_idt> codes;
76 while(next_id > end_id)
77 {
78 auto node = scope_graph[next_id];
79 auto &destructor = node.destructor_value;
80 if(destructor)
81 codes.emplace_back(destructor_and_idt(*destructor, next_id));
82
83 next_id = node.in.begin()->first;
84 }
85
86 return codes;
87}
88
89void scope_treet::set_current_node(std::optional<node_indext> val)
90{
91 if(val)
93}
94
99
101{
103 if(current_node != 0)
104 {
105 set_current_node(scope_graph[current_node].in.begin()->first);
106 }
107}
108
113
115 codet destructor,
116 std::optional<declaration_statet> declaration)
117 : destructor_value(std::move(destructor)), declaration(std::move(declaration))
118{
119}
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
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 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 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.
STL namespace.
std::size_t node_indext
Definition scope_tree.h:19
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423