Use format rather than from_expr for output

Author: thk123

src/cbmc/bmc.h

@@ -78,7 +78,7 @@ class bmct:public safety_checkert
       options(_options),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table, symex_symbol_table),
-      equation(ns),
+      equation(),
       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(ns),
+      equation(),
       branch_worklist(),
       symex(mh, symbol_table, equation, branch_worklist),
       satcheck(util_make_unique<satcheckt>()),

src/goto-symex/equation_conversion_exceptions.h

@@ -14,9 +14,7 @@ Author: Diffblue Ltd.
 
 #include <ostream>
 
-#include <util/namespace.h>
-
-#include <langapi/language_util.h>
+#include <util/format.h>
 
 #include "symex_target_equation.h"
 
@@ -25,26 +23,17 @@ class equation_conversion_exceptiont : public std::runtime_error
 public:
   equation_conversion_exceptiont(
     const std::string &message,
-    const symex_target_equationt::SSA_stept &step,
-    const namespacet &ns)
+    const symex_target_equationt::SSA_stept &step)
     : runtime_error(message), step(step)
   {
     std::ostringstream error_msg;
     error_msg << runtime_error::what();
-    error_msg << "\nSource GOTO statement: "
-              << from_expr(ns, "java", step.source.pc->code);
+    error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
     error_msg << "\nStep:\n";
-    step.output(ns, error_msg);
+    step.output(error_msg);
     error_message = error_msg.str();
   }
 
-  explicit equation_conversion_exceptiont(
-    const std::string &message,
-    const symex_target_equationt::SSA_stept &step)
-    : equation_conversion_exceptiont(message, step, namespacet{symbol_tablet{}})
-  {
-  }
-
   const char *what() const optional_noexcept override
   {
     return error_message.c_str();

src/goto-symex/symex_target_equation.cpp

@@ -11,11 +11,15 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target_equation.h"
 
+#include <util/format.h>
+#include <util/format_expr.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
 
+// Can be removed once deprecated SSA_stept::output is removed
 #include <langapi/language_util.h>
+
 #include <solvers/flattening/bv_conversion_exceptions.h>
 #include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop.h>
@@ -423,7 +427,7 @@ void symex_target_equationt::convert_decls(
       {
         util_throw_with_nested(
           equation_conversion_exceptiont(
-            "Error converting decls for step", step, ns));
+            "Error converting decls for step", step));
       }
     }
   }
@@ -448,7 +452,7 @@ void symex_target_equationt::convert_guards(
       {
         util_throw_with_nested(
           equation_conversion_exceptiont(
-            "Error converting guard for step", step, ns));
+            "Error converting guard for step", step));
       }
     }
   }
@@ -475,7 +479,7 @@ void symex_target_equationt::convert_assumptions(
         {
           util_throw_with_nested(
             equation_conversion_exceptiont(
-              "Error converting assumptions for step", step, ns));
+              "Error converting assumptions for step", step));
         }
       }
     }
@@ -503,7 +507,7 @@ void symex_target_equationt::convert_goto_instructions(
         {
           util_throw_with_nested(
             equation_conversion_exceptiont(
-              "Error converting goto instructions for step", step, ns));
+              "Error converting goto instructions for step", step));
         }
       }
     }
@@ -582,7 +586,7 @@ void symex_target_equationt::convert_assertions(
       {
         util_throw_with_nested(
           equation_conversion_exceptiont(
-            "Error converting assertions for step", step, ns));
+            "Error converting assertions for step", step));
       }
 
       // store disjunct
@@ -767,3 +771,101 @@ void symex_target_equationt::SSA_stept::output(
 
   out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
 }
+
+void symex_target_equationt::SSA_stept::output(std::ostream &out) const
+{
+  if(source.is_set)
+  {
+    out << "Thread " << source.thread_nr;
+
+    if(source.pc->source_location.is_not_nil())
+      out << " " << source.pc->source_location << '\n';
+    else
+      out << '\n';
+  }
+
+  switch(type)
+  {
+  case goto_trace_stept::typet::ASSERT:
+    out << "ASSERT " << format(cond_expr) << '\n'; break;
+  case goto_trace_stept::typet::ASSUME:
+    out << "ASSUME " << format(cond_expr) << '\n'; break;
+  case goto_trace_stept::typet::LOCATION:
+    out << "LOCATION" << '\n'; break;
+  case goto_trace_stept::typet::INPUT:
+    out << "INPUT" << '\n'; break;
+  case goto_trace_stept::typet::OUTPUT:
+    out << "OUTPUT" << '\n'; break;
+
+  case goto_trace_stept::typet::DECL:
+    out << "DECL" << '\n';
+    out << format(ssa_lhs) << '\n';
+    break;
+
+  case goto_trace_stept::typet::ASSIGNMENT:
+    out << "ASSIGNMENT (";
+    switch(assignment_type)
+    {
+    case assignment_typet::HIDDEN:
+      out << "HIDDEN";
+      break;
+    case assignment_typet::STATE:
+      out << "STATE";
+      break;
+    case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
+      out << "VISIBLE_ACTUAL_PARAMETER";
+      break;
+    case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
+      out << "HIDDEN_ACTUAL_PARAMETER";
+      break;
+    case assignment_typet::PHI:
+      out << "PHI";
+      break;
+    case assignment_typet::GUARD:
+      out << "GUARD";
+      break;
+    default:
+    {
+    }
+    }
+
+    out << ")\n";
+    break;
+
+  case goto_trace_stept::typet::DEAD:
+    out << "DEAD\n"; break;
+  case goto_trace_stept::typet::FUNCTION_CALL:
+    out << "FUNCTION_CALL\n"; break;
+  case goto_trace_stept::typet::FUNCTION_RETURN:
+    out << "FUNCTION_RETURN\n"; break;
+  case goto_trace_stept::typet::CONSTRAINT:
+    out << "CONSTRAINT\n"; break;
+  case goto_trace_stept::typet::SHARED_READ:
+    out << "SHARED READ\n"; break;
+  case goto_trace_stept::typet::SHARED_WRITE:
+    out << "SHARED WRITE\n"; break;
+  case goto_trace_stept::typet::ATOMIC_BEGIN:
+    out << "ATOMIC_BEGIN\n"; break;
+  case goto_trace_stept::typet::ATOMIC_END:
+    out << "AUTOMIC_END\n"; break;
+  case goto_trace_stept::typet::SPAWN:
+    out << "SPAWN\n"; break;
+  case goto_trace_stept::typet::MEMORY_BARRIER:
+    out << "MEMORY_BARRIER\n"; break;
+  case goto_trace_stept::typet::GOTO:
+    out << "IF " << format(cond_expr) << " GOTO\n"; break;
+
+  default: UNREACHABLE;
+  }
+
+  if(is_assert() || is_assume() || is_assignment() || is_constraint())
+    out << format(cond_expr) << '\n';
+
+  if(is_assert() || is_constraint())
+    out << comment << '\n';
+
+  if(is_shared_read() || is_shared_write())
+    out << format(ssa_lhs) << '\n';
+
+  out << "Guard: " << format(guard) << '\n';
+}

src/goto-symex/symex_target_equation.h

@@ -32,10 +32,7 @@ class prop_convt;
 class symex_target_equationt:public symex_targett
 {
 public:
-  explicit symex_target_equationt(const namespacet &ns) : ns(ns)
-  {
-  }
-
+  symex_target_equationt() = default;
   virtual ~symex_target_equationt() = default;
 
   // read event
@@ -260,9 +257,12 @@ class symex_target_equationt:public symex_targett
     {
     }
 
+    DEPRECATED("Use output without ns param")
     void output(
       const namespacet &ns,
       std::ostream &out) const;
+
+    void output(std::ostream &out) const;
   };
 
   std::size_t count_assertions() const
@@ -323,9 +323,6 @@ 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<(