Skip to content

Commit c96b3b2

Browse files
committed
Implement storage of declaration iterator in scope_tree nodes
So it can be retrieved when producing the code for jumping into a scope.
1 parent be3a32f commit c96b3b2

File tree

2 files changed

+24
-5
lines changed

2 files changed

+24
-5
lines changed

src/goto-programs/scope_tree.cpp

+16-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ void scope_treet::add(
1313
std::optional<goto_programt::targett> declaration)
1414
{
1515
auto previous_node = get_current_node();
16-
auto new_node = scope_graph.add_node(destructor);
16+
auto new_node = scope_graph.add_node(destructor, declaration);
1717
scope_graph.add_edge(previous_node, new_node);
1818
current_node = new_node;
1919
}
@@ -24,6 +24,13 @@ optionalt<codet> &scope_treet::get_destructor(node_indext index)
2424
return scope_graph[index].destructor_value;
2525
}
2626

27+
optionalt<goto_programt::targett> &
28+
scope_treet::get_declaration(node_indext index)
29+
{
30+
PRECONDITION(index < scope_graph.size());
31+
return scope_graph[index].declaration_value;
32+
}
33+
2734
const ancestry_resultt scope_treet::get_nearest_common_ancestor_info(
2835
node_indext left_index,
2936
node_indext right_index)
@@ -100,3 +107,11 @@ node_indext scope_treet::get_current_node() const
100107
{
101108
return current_node;
102109
}
110+
111+
scope_treet::scope_nodet::scope_nodet(
112+
codet destructor,
113+
std::optional<goto_programt::targett> declaration)
114+
: destructor_value(std::move(destructor)),
115+
declaration_value(std::move(declaration))
116+
{
117+
}

src/goto-programs/scope_tree.h

+8-4
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,9 @@ class scope_treet
107107
/// Fetches the destructor value for the passed-in node index.
108108
optionalt<codet> &get_destructor(node_indext index);
109109

110+
/// Fetches the declaration value for the passed-in node index.
111+
optionalt<goto_programt::targett> &get_declaration(node_indext index);
112+
110113
/// Builds a vector of destructors that start from starting_index and ends
111114
/// at end_index.
112115
/// \param end_index Index of the first variable to keep.
@@ -147,11 +150,12 @@ class scope_treet
147150
public:
148151
scope_nodet() = default;
149152

150-
explicit scope_nodet(codet destructor)
151-
: destructor_value(std::move(destructor))
152-
{
153-
}
153+
explicit scope_nodet(
154+
codet destructor,
155+
std::optional<goto_programt::targett> declaration);
156+
154157
optionalt<codet> destructor_value;
158+
optionalt<goto_programt::targett> declaration_value;
155159
};
156160

157161
grapht<scope_nodet> scope_graph;

0 commit comments

Comments
 (0)