Fix for cbmc running out of memory while printing traces using json_ui

src/cbmc/all_properties.cpp

@@ -207,24 +207,24 @@ 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);
+          json_stream_arrayt &json_trace=result.push_back_stream_array("trace");
+          convert<json_stream_arrayt>(bmc.ns, g.second.goto_trace, json_trace);
         }
       }
-
-      std::cout << ",\n" << json_result;
     }
     break;
   }

src/cbmc/bmc.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/time_stopping.h>
 #include <util/message.h>
 #include <util/json.h>
+#include <util/json_stream.h>
 #include <util/cprover_prefix.h>
 
 #include <langapi/mode.h>
@@ -71,18 +72,17 @@ void bmct::error_trace()
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_arrayt &result_array=json_result["results"].make_array();
-      json_objectt &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();
-      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");
-      jsont &json_trace=result["trace"];
-      convert(ns, goto_trace, json_trace);
-      std::cout << ",\n" << json_result;
+      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/cbmc/bmc_cover.cpp

@@ -378,7 +378,7 @@ 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=result["trace"].make_array();
           convert(bmc.ns, test.goto_trace, json_trace);
         }
         else