Merge pull request #3961 from tautschnig/fix-3956-namespace

Restore namespace after symbolic execution [blocks: #3976]

Author: tautschnig

regression/cbmc/coverage_report1/paths.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--symex-coverage-report - --paths lifo
+<line branch="false" hits="1" number="12"/>
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/symex_main.cpp

@@ -254,12 +254,34 @@ void goto_symext::symex_with_state(
   const get_goto_functiont &get_goto_function,
   symbol_tablet &new_symbol_table)
 {
+  // resets the namespace to only wrap a single symbol table, and does so upon
+  // destruction of an object of this type; instantiating the type is thus all
+  // that's needed to achieve a reset upon exiting this method
+  struct reset_namespacet
+  {
+    explicit reset_namespacet(namespacet &ns) : ns(ns)
+    {
+    }
+
+    ~reset_namespacet()
+    {
+      const symbol_tablet &st = ns.get_symbol_table();
+      ns = namespacet(st);
+    }
+
+    namespacet &ns;
+  };
+
   // We'll be using ns during symbolic execution and it needs to know
   // about the names minted in `state`, so make it point both to
   // `state`'s symbol table and the symbol table of the original
   // goto-program.
   ns = namespacet(outer_symbol_table, state.symbol_table);
 
+  // whichever way we exit this method, reset the namespace back to a sane state
+  // as state.symbol_table might go out of scope
+  reset_namespacet reset_ns(ns);
+
   PRECONDITION(state.top().end_of_function->is_end_function());
 
   symex_threaded_step(state, get_goto_function);
@@ -279,9 +301,6 @@ void goto_symext::symex_with_state(
   // execution, so return the names generated through symbolic execution
   // through `new_symbol_table`.
   new_symbol_table = state.symbol_table;
-  // reset the namespace back to a sane state as state.symbol_table might go out
-  // of scope
-  ns = namespacet(outer_symbol_table);
 }
 
 void goto_symext::resume_symex_from_saved_state(