Provide the original goto statement in the error

This required the symex target_equation having the namespace to resolve
names

Author: thk123

src/cbmc/bmc.h

@@ -80,7 +80,7 @@ class bmct:public safety_checkert
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table, symex_symbol_table),
-      equation(),
+      equation(ns),
       branch_worklist(_branch_worklist),
       symex(_message_handler, outer_symbol_table, equation, branch_worklist),
       prop_conv(_prop_conv),

src/goto-instrument/accelerate/scratch_program.h

@@ -40,7 +40,7 @@ class scratch_programt:public goto_programt
       symbol_table(_symbol_table),
       symex_symbol_table(),
       ns(symbol_table, symex_symbol_table),
-      equation(),
+      equation(ns),
       branch_worklist(),
       symex(mh, symbol_table, equation, branch_worklist),
       satcheck(util_make_unique<satcheckt>()),

src/goto-symex/equation_conversion_exceptions.h

@@ -14,6 +14,7 @@ Author: Diffblue Ltd.
 
 #include <ostream>
 #include <util/namespace.h>
+#include <langapi/language_util.h>
 #include "symex_target_equation.h"
 
 class guard_conversion_exceptiont : public std::runtime_error
@@ -26,6 +27,8 @@ class guard_conversion_exceptiont : public std::runtime_error
   {
     std::ostringstream error_msg;
     error_msg << runtime_error::what();
+    error_msg << "\nSource GOTO statement: "
+              << from_expr(ns, "java", step.source.pc->code);
     error_msg << "\nStep:\n";
     step.output(ns, error_msg);
     error_message = error_msg.str();

src/goto-symex/symex_target_equation.cpp

@@ -439,7 +439,7 @@ void symex_target_equationt::convert_guards(
       }
       catch(const bitvector_conversion_exceptiont &conversion_exception)
       {
-        std::throw_with_nested(guard_conversion_exceptiont(step));
+        std::throw_with_nested(guard_conversion_exceptiont(step, ns));
       }
     }
   }

src/goto-symex/symex_target_equation.h

@@ -32,7 +32,9 @@ class prop_convt;
 class symex_target_equationt:public symex_targett
 {
 public:
-  symex_target_equationt() = default;
+  symex_target_equationt(const namespacet &ns) : ns(ns)
+  { }
+
   virtual ~symex_target_equationt() = default;
 
   // read event
@@ -320,6 +322,9 @@ class symex_target_equationt:public symex_targett
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;
   void merge_ireps(SSA_stept &SSA_step);
+
+private:
+  const namespacet &ns;
 };
 
 inline bool operator<(