Extend declaration in scope tree into a stateful struct

So that we can track what changes have been made to each declaration.

Author: thomasspriggs

Diff for: src/goto-programs/scope_tree.cpp

@@ -13,7 +13,10 @@ void scope_treet::add(
   std::optional<goto_programt::targett> declaration)
 {
   auto previous_node = get_current_node();
-  auto new_node = scope_graph.add_node(destructor, declaration);
+  using declaration_optt = std::optional<declaration_statet>;
+  auto declaration_opt =
+    declaration ? declaration_optt{{*declaration}} : declaration_optt{};
+  auto new_node = scope_graph.add_node(destructor, std::move(declaration_opt));
   scope_graph.add_edge(previous_node, new_node);
   current_node = new_node;
 }
@@ -24,11 +27,11 @@ optionalt<codet> &scope_treet::get_destructor(node_indext index)
   return scope_graph[index].destructor_value;
 }
 
-optionalt<goto_programt::targett> &
+optionalt<scope_treet::declaration_statet> &
 scope_treet::get_declaration(node_indext index)
 {
   PRECONDITION(index < scope_graph.size());
-  return scope_graph[index].declaration_value;
+  return scope_graph[index].declaration;
 }
 
 const ancestry_resultt scope_treet::get_nearest_common_ancestor_info(
@@ -110,8 +113,7 @@ node_indext scope_treet::get_current_node() const
 
 scope_treet::scope_nodet::scope_nodet(
   codet destructor,
-  std::optional<goto_programt::targett> declaration)
-  : destructor_value(std::move(destructor)),
-    declaration_value(std::move(declaration))
+  std::optional<declaration_statet> declaration)
+  : destructor_value(std::move(destructor)), declaration(std::move(declaration))
 {
 }

Diff for: src/goto-programs/scope_tree.h

@@ -14,6 +14,8 @@
 
 #include <goto-programs/goto_program.h>
 
+#include <unordered_set>
+
 typedef std::size_t node_indext;
 
 /// Result of an attempt to find ancestor information about two nodes. Holds
@@ -90,6 +92,12 @@ class destructor_and_idt
 class scope_treet
 {
 public:
+  struct declaration_statet
+  {
+    goto_programt::targett instruction;
+    std::unordered_set<irep_idt, irep_id_hash> if_conditions_added;
+  };
+
   scope_treet()
   {
     // We add a default node to the graph to act as a root for path traversal.
@@ -108,7 +116,7 @@ class scope_treet
   optionalt<codet> &get_destructor(node_indext index);
 
   /// Fetches the declaration value for the passed-in node index.
-  optionalt<goto_programt::targett> &get_declaration(node_indext index);
+  optionalt<declaration_statet> &get_declaration(node_indext index);
 
   /// Builds a vector of destructors that start from starting_index and ends
   /// at end_index.
@@ -152,10 +160,10 @@ class scope_treet
 
     explicit scope_nodet(
       codet destructor,
-      std::optional<goto_programt::targett> declaration);
+      std::optional<declaration_statet> declaration);
 
     optionalt<codet> destructor_value;
-    optionalt<goto_programt::targett> declaration_value;
+    optionalt<declaration_statet> declaration;
   };
 
   grapht<scope_nodet> scope_graph;