Restrict get_json_stream to ui_message_handler

... now that we properly pass around ui_message_handlert we can clean up the
JSON stream handling as well.

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -202,8 +202,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 
     case ui_message_handlert::uit::JSON_UI:
     {
+      if(result().tellp() > 0)
+        result() << eom; // force end of previous message
       json_stream_objectt &json_result =
-        result().json_stream().push_back_stream_object();
+        bmc.ui_message_handler.get_json_stream().push_back_stream_object();
       json_stream_arrayt &result_array =
         json_result.push_back_stream_array("result");
 

src/cbmc/bmc.cpp

@@ -72,8 +72,10 @@ void bmct::error_trace()
 
   case ui_message_handlert::uit::JSON_UI:
     {
+      if(status().tellp() > 0)
+        status() << eom; // force end of previous message
       json_stream_objectt &json_result =
-        status().json_stream().push_back_stream_object();
+        ui_message_handler.get_json_stream().push_back_stream_object();
       const goto_trace_stept &step=goto_trace.steps.back();
       json_result["property"] =
         json_stringt(step.pc->source_location.get_property_id());

src/cbmc/bmc_cover.cpp

@@ -341,8 +341,10 @@ bool bmc_covert::operator()()
 
     case ui_message_handlert::uit::JSON_UI:
     {
+      if(status().tellp() > 0)
+        status() << eom; // force end of previous message
       json_stream_objectt &json_result =
-        status().json_stream().push_back_stream_object();
+        bmc.ui_message_handler.get_json_stream().push_back_stream_object();
       for(const auto &goal_pair : goal_map)
       {
         const goalt &goal=goal_pair.second;

src/goto-programs/class_hierarchy.cpp

@@ -273,7 +273,9 @@ void show_class_hierarchy(
     msg.result() << messaget::eom;
     break;
   case ui_message_handlert::uit::JSON_UI:
-    hierarchy.output(msg.result().json_stream(), children_only);
+    if(msg.result().tellp() > 0)
+      msg.result() << messaget::eom; // force end of previous message
+    hierarchy.output(message_handler.get_json_stream(), children_only);
     break;
   case ui_message_handlert::uit::XML_UI:
     UNIMPLEMENTED;

src/util/message.h

@@ -18,9 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "invariant.h"
 #include "json.h"
 #include "source_location.h"
-#include "xml.h"
 
-class json_stream_arrayt;
+class xmlt;
 
 class message_handlert
 {
@@ -36,12 +35,6 @@ class message_handlert
     // no-op by default
   }
 
-  /// Return the underlying JSON stream
-  virtual json_stream_arrayt &get_json_stream()
-  {
-    UNREACHABLE;
-  }
-
   virtual void print(unsigned level, const jsont &json)
   {
     // no-op by default
@@ -246,14 +239,6 @@ class messaget
       return func(*this);
     }
 
-    /// Returns a reference to the top-level JSON array stream
-    json_stream_arrayt &json_stream()
-    {
-      if(this->tellp() > 0)
-        *this << eom; // force end of previous message
-      return message.message_handler->get_json_stream();
-    }
-
   private:
     void assign_from(const mstreamt &other)
     {

src/util/ui_message.cpp

@@ -61,13 +61,8 @@ ui_message_handlert::ui_message_handlert(
 
   case uit::JSON_UI:
     {
-      if(!json_stream)
-      {
-        json_stream =
-          std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
-      }
-
-      INVARIANT(json_stream, "JSON stream must be initialized before use");
+      json_stream =
+        std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
       json_stream->push_back().make_object()["program"] = json_stringt(program);
     }
     break;

src/util/ui_message.h

@@ -41,7 +41,7 @@ class ui_message_handlert : public message_handlert
 
   virtual void flush(unsigned level) override;
 
-  json_stream_arrayt &get_json_stream() override
+  json_stream_arrayt &get_json_stream()
   {
     PRECONDITION(json_stream!=nullptr);
     return *json_stream;