Update interface of destructor_treet::add to add a declaration

Because this will be needed later for entering a scope via a C front end
goto statement. The declaration is optional because it is only needed
for named front end declarations. It is not needed for anonymous symbols
which cannot be referenced by user code.

Author: thomasspriggs

src/goto-programs/destructor_tree.cpp

@@ -8,7 +8,9 @@
 
 #include "destructor_tree.h"
 
-void destructor_treet::add(const codet &destructor)
+void destructor_treet::add(
+  const codet &destructor,
+  std::optional<goto_programt::targett> declaration)
 {
   auto previous_node = get_current_node();
   auto new_node = destruction_graph.add_node(destructor);

src/goto-programs/destructor_tree.h

@@ -12,6 +12,8 @@
 #include <util/graph.h>
 #include <util/std_code_base.h>
 
+#include <goto-programs/goto_program.h>
+
 typedef std::size_t node_indext;
 
 /// Result of an attempt to find ancestor information about two nodes. Holds
@@ -94,9 +96,13 @@ class destructor_treet
     this->destruction_graph.add_node();
   }
 
-  /// Adds a destructor to the current stack, attaching itself to the
-  /// current node.
-  void add(const codet &destructor);
+  /// Adds a destructor/declaration pair to the current stack, attaching it to
+  /// the current node.
+  /// \param destructor Code which is called when the current scope is left.
+  /// \param declaration Instruction which causes the scope to be entered.
+  void add(
+    const codet &destructor,
+    std::optional<goto_programt::targett> declaration);
 
   /// Fetches the destructor value for the passed-in node index.
   optionalt<codet> &get_destructor(node_indext index);

src/goto-programs/goto_clean_expr.cpp

@@ -53,7 +53,7 @@ symbol_exprt goto_convertt::make_compound_literal(
   if(!new_symbol.is_static_lifetime)
   {
     code_deadt code_dead(result);
-    targets.destructor_stack.add(std::move(code_dead));
+    targets.destructor_stack.add(std::move(code_dead), {});
   }
 
   return result;

src/goto-programs/goto_convert.cpp

@@ -653,7 +653,7 @@ void goto_convertt::convert_frontend_decl(
 
   {
     code_deadt code_dead(symbol_expr);
-    targets.destructor_stack.add(code_dead);
+    targets.destructor_stack.add(code_dead, {});
   }
 
   // do destructor
@@ -665,7 +665,7 @@ void goto_convertt::convert_frontend_decl(
     address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
     destructor.arguments().push_back(this_expr);
 
-    targets.destructor_stack.add(destructor);
+    targets.destructor_stack.add(destructor, {});
   }
 }
 

src/goto-programs/goto_convert_exceptions.cpp

@@ -34,7 +34,7 @@ void goto_convertt::convert_msc_try_finally(
 
     // first put 'finally' code onto destructor stack
     node_indext old_stack_top = targets.destructor_stack.get_current_node();
-    targets.destructor_stack.add(to_code(code.op1()));
+    targets.destructor_stack.add(to_code(code.op1()), {});
 
     // do 'try' code
     convert(to_code(code.op0()), dest, mode);
@@ -166,7 +166,7 @@ void goto_convertt::convert_CPROVER_try_catch(
 
   // Store the point before the temp catch code.
   node_indext old_stack_top = targets.destructor_stack.get_current_node();
-  targets.destructor_stack.add(catch_code);
+  targets.destructor_stack.add(catch_code, {});
 
   // now convert 'try' code
   convert(to_code(code.op0()), dest, mode);
@@ -221,7 +221,7 @@ void goto_convertt::convert_CPROVER_try_finally(
 
   // first put 'finally' code onto destructor stack
   node_indext old_stack_top = targets.destructor_stack.get_current_node();
-  targets.destructor_stack.add(to_code(code.op1()));
+  targets.destructor_stack.add(to_code(code.op1()), {});
 
   // do 'try' code
   convert(to_code(code.op0()), dest, mode);