Activate JSON streaming when printing goto-traces

Author: NlightNFotis

src/cbmc/all_properties.cpp

@@ -206,24 +206,26 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_arrayt &result_array=json_result["result"].make_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)
       {
-        json_objectt &result=result_array.push_back().make_object();
+        json_stream_objectt &result = result_array.push_back_stream_object();
         result["property"]=json_stringt(id2string(g.first));
         result["description"]=json_stringt(id2string(g.second.description));
         result["status"]=json_stringt(g.second.status_string());
 
         if(g.second.status==goalt::statust::FAILURE)
         {
-          jsont &json_trace=result["trace"];
-          convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
+          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());
         }
       }
-
-      result() << json_result;
     }
     break;
   }

src/cbmc/bmc.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/memory_info.h>
 #include <util/message.h>
 #include <util/json.h>
+#include <util/json_stream.h>
 #include <util/cprover_prefix.h>
 
 #include <langapi/mode.h>
@@ -86,18 +87,17 @@ void bmct::error_trace()
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json;
-      json_arrayt &result_array=json["results"].make_array();
-      json_objectt &json_result=result_array.push_back().make_object();
+      json_stream_objectt &json_result =
+        status().json_stream().push_back_stream_object();
       const goto_trace_stept &step=goto_trace.steps.back();
       json_result["property"]=
         json_stringt(id2string(step.pc->source_location.get_property_id()));
       json_result["description"]=
         json_stringt(id2string(step.pc->source_location.get_comment()));
       json_result["status"]=json_stringt("failed");
-      jsont &json_trace=json_result["trace"];
-      convert(ns, goto_trace, json_trace, trace_options());
-      status() << json_result;
+      json_stream_arrayt &json_trace =
+        json_result.push_back_stream_array("trace");
+      convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options());
     }
     break;
   }

src/cbmc/bmc_cover.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/xml.h>
 #include <util/xml_expr.h>
 #include <util/json.h>
+#include <util/json_stream.h>
 #include <util/json_expr.h>
 
 #include <solvers/prop/cover_goals.h>
@@ -346,19 +347,19 @@ bool bmc_covert::operator()()
 
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_arrayt &goals_array=json_result["goals"].make_array();
+      json_stream_objectt &json_result =
+        status().json_stream().push_back_stream_object();
       for(const auto &goal_pair : goal_map)
       {
         const goalt &goal=goal_pair.second;
 
-        json_objectt &result=goals_array.push_back().make_object();
-        result["status"]=json_stringt(goal.satisfied?"satisfied":"failed");
-        result["goal"]=json_stringt(id2string(goal_pair.first));
-        result["description"]=json_stringt(goal.description);
+        json_result["status"] =
+          json_stringt(goal.satisfied ? "satisfied" : "failed");
+        json_result["goal"] = json_stringt(id2string(goal_pair.first));
+        json_result["description"] = json_stringt(goal.description);
 
         if(goal.source_location.is_not_nil())
-          result["sourceLocation"]=json(goal.source_location);
+          json_result["sourceLocation"] = json(goal.source_location);
       }
       json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
       json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
@@ -369,12 +370,12 @@ bool bmc_covert::operator()()
         json_objectt &result=tests_array.push_back().make_object();
         if(bmc.options.get_bool_option("trace"))
         {
-          jsont &json_trace=result["trace"];
+          json_arrayt &json_trace = json_result["trace"].make_array();
           convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
         }
         else
         {
-          json_arrayt &json_test=result["inputs"].make_array();
+          json_arrayt &json_test = json_result["inputs"].make_array();
 
           for(const auto &step : test.goto_trace.steps)
           {
@@ -396,7 +397,6 @@ bool bmc_covert::operator()()
         }
       }
 
-      result() << json_result;
       break;
     }
   }

src/goto-programs/interpreter.cpp

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <json/json_parser.h>
 
 #include "interpreter_class.h"
+#include "json_goto_trace.h"
 #include "remove_returns.h"
 
 const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
@@ -151,8 +152,8 @@ void interpretert::command()
   }
   else if(ch=='j')
   {
-    jsont json_steps;
-    convert(ns, steps, json_steps);
+    json_arrayt json_steps;
+    convert<json_arrayt>(ns, steps, json_steps);
     ch=tolower(command[1]);
     if(ch==' ')
     {