From 23196afcf403541ba54f53c16227b45cf40a0426 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 26 Jan 2019 23:10:00 +0000
Subject: [PATCH] Restore namespace after symbolic execution

This was already fixed in d475abcdb9268, but 685937a79e introduced additional
returns. Now use an approach that will always work, even when returning via
exceptions being thrown.
---
 regression/cbmc/coverage_report1/paths.desc |  9 ++++++++
 src/goto-symex/symex_main.cpp               | 25 ++++++++++++++++++---
 2 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/coverage_report1/paths.desc

diff --git a/regression/cbmc/coverage_report1/paths.desc b/regression/cbmc/coverage_report1/paths.desc
new file mode 100644
index 00000000000..6a5b7a085d3
--- /dev/null
+++ b/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
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 9e038616303..836845364c3 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/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(