Make ui_message_handlert the only class to provide a json_stream

It always was the only place that had one, but various other APIs claimed they
did so as well.

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -207,7 +207,7 @@ 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();
+        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

@@ -70,7 +70,7 @@ void bmct::error_trace()
   case ui_message_handlert::uit::JSON_UI:
     {
       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

@@ -348,7 +348,7 @@ bool bmc_covert::operator()()
     case ui_message_handlert::uit::JSON_UI:
     {
       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

@@ -206,7 +206,7 @@ void show_class_hierarchy(
     msg.result() << messaget::eom;
     break;
   case ui_message_handlert::uit::JSON_UI:
-    hierarchy.output(msg.result().json_stream(), children_only);
+    hierarchy.output(message_handler.get_json_stream(), children_only);
     break;
   case ui_message_handlert::uit::XML_UI:
     UNIMPLEMENTED;

src/util/message.h

@@ -36,12 +36,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
@@ -248,14 +242,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.h

@@ -51,7 +51,8 @@ class ui_message_handlert : public message_handlert
 
   virtual void flush(unsigned level) override;
 
-  json_stream_arrayt &get_json_stream() override
+  /// Return the underlying JSON stream
+  json_stream_arrayt &get_json_stream()
   {
     PRECONDITION(json_stream!=nullptr);
     return *json_stream;