Implement necessary changes for goto-analyzer-develop branch.

Author: NlightNFotis

src/cbmc/all_properties.cpp

@@ -207,8 +207,9 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_stream_objectt &json_result = result().json_stream().push_back_stream_object();
-      json_stream_arrayt &result_array =
+      json_stream_objectt &json_result=
+        result().json_stream().push_back_stream_object();
+      json_stream_arrayt &result_array=
         json_result.push_back_stream_array("result");
 
       for(const auto &g : goal_map)
@@ -221,7 +222,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         if(g.second.status==goalt::statust::FAILURE)
         {
           json_stream_arrayt &json_trace=result.push_back_stream_array("trace");
-          convert<json_stream_arrayt>(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
+          convert<json_stream_arrayt>(bmc.ns, g.second.goto_trace, json_trace);
         }
       }
     }

src/cbmc/bmc.cpp

@@ -72,15 +72,17 @@ void bmct::error_trace()
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_stream_objectt &json_result = status().json_stream().push_back_stream_object();
+      json_stream_objectt &json_result=
+        status().json_stream().push_back_stream_object();
       const goto_trace_stept &step=goto_trace.steps.back();
-      result["property"]=
+      json_result["property"]=
         json_stringt(id2string(step.pc->source_location.get_property_id()));
-      result["description"]=
+      json_result["description"]=
         json_stringt(id2string(step.pc->source_location.get_comment()));
-      result["status"]=json_stringt("failed");
-      json_stream_arrayt &json_trace=json_result.push_back_stream_array("trace");
-      convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options());
+      json_result["status"]=json_stringt("failed");
+      json_stream_arrayt &json_trace=
+        json_result.push_back_stream_array("trace");
+      convert<json_stream_arrayt>(ns, goto_trace, json_trace);
     }
     break;
   }

src/goto-programs/interpreter.cpp

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "interpreter.h"
 #include "interpreter_class.h"
-#include "json_goto_trace.h"
 
 void interpretert::operator()()
 {
@@ -80,8 +79,6 @@ void interpretert::command()
 
   if(ch=='q')
     done=true;
-    json_arrayt json_steps;
-    convert<json_arrayt>(ns, steps, json_steps);
 }
 
 void interpretert::step()

src/goto-programs/json_goto_trace.cpp

@@ -11,18 +11,12 @@ Author: Daniel Kroening
 /// \file
 /// Traces of GOTO Programs
 
+#include <cassert>
+
+#include <util/json_expr.h>
+
+#include <langapi/language_util.h>
+
 #include "json_goto_trace.h"
-/// Produce a json representation of a trace.
-/// \param ns: a namespace
-  jsont &dest,
-
-        DATA_INVARIANT(
-          step.full_lhs.is_not_nil(),
-            void operator()(exprt &expr) override
-            {
-              if(expr.id() == ID_symbol)
-              {
-        full_lhs_string=from_expr(ns, identifier, simplified);
-          full_lhs_value = json(step.full_lhs_value, ns);
-            json_values.push_back(json(arg, ns, mode));
-            json_values.push_back(json(arg, ns, mode));
+
+