Make message streams accept XML and JSON data

src/analyses/natural_loops.cpp

@@ -11,18 +11,18 @@ Author: Georg Weissenbacher, [email protected]
 
 #include "natural_loops.h"
 
-#include <iostream>
-
-void show_natural_loops(const goto_modelt &goto_model)
+void show_natural_loops(
+  const goto_modelt &goto_model,
+  std::ostream &out)
 {
   forall_goto_functions(it, goto_model.goto_functions)
   {
-    std::cout << "*** " << it->first << '\n';
+    out << "*** " << it->first << '\n';
 
     natural_loopst natural_loops;
     natural_loops(it->second.body);
-    natural_loops.output(std::cout);
+    natural_loops.output(out);
 
-    std::cout << '\n';
+    out << '\n';
   }
 }

src/analyses/natural_loops.h

@@ -69,7 +69,9 @@ class natural_loopst:
 typedef natural_loops_templatet<goto_programt, goto_programt::targett>
     natural_loops_mutablet;
 
-void show_natural_loops(const goto_modelt &);
+void show_natural_loops(
+  const goto_modelt &,
+  std::ostream &out);
 
 /// Finds all back-edges and computes the natural loops
 #ifdef DEBUG

src/cbmc/all_properties.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "all_properties_class.h"
 
-#include <iostream>
-
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/json.h>
@@ -163,10 +161,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
   {
   case ui_message_handlert::uit::PLAIN:
     {
-      status() << "\n** Results:" << eom;
+      result() << "\n** Results:" << eom;
 
       for(const auto &goal_pair : goal_map)
-        status() << "[" << goal_pair.first << "] "
+        result() << "[" << goal_pair.first << "] "
                  << goal_pair.second.description << ": "
                  << goal_pair.second.status_string()
                  << eom;
@@ -176,10 +174,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         for(const auto &g : goal_map)
           if(g.second.status==goalt::statust::FAILURE)
           {
-            std::cout << "\n" << "Trace for " << g.first << ":" << "\n";
-            show_goto_trace(std::cout, bmc.ns, g.second.goto_trace);
+            result() << "\n" << "Trace for " << g.first << ":" << "\n";
+            show_goto_trace(result(), bmc.ns, g.second.goto_trace);
           }
       }
+      result() << eom;
 
       status() << "\n** " << cover_goals.number_covered()
                << " of " << cover_goals.size() << " failed ("
@@ -200,7 +199,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         if(g.second.status==goalt::statust::FAILURE)
           convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -224,7 +223,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         }
       }
 
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }

src/cbmc/bmc.cpp

@@ -55,33 +55,33 @@ void bmct::error_trace()
   switch(ui)
   {
   case ui_message_handlert::uit::PLAIN:
-    status() << "Counterexample:" << eom;
-    show_goto_trace(status(), ns, goto_trace);
-    status() << eom;
+    result() << "Counterexample:" << eom;
+    show_goto_trace(result(), ns, goto_trace);
+    result() << eom;
     break;
 
   case ui_message_handlert::uit::XML_UI:
     {
       xmlt xml;
       convert(ns, goto_trace, xml);
-      status() << preformatted_output << xml << eom;
+      status() << xml;
     }
     break;
 
   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_objectt json;
+      json_arrayt &result_array=json["results"].make_array();
+      json_objectt &json_result=result_array.push_back().make_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"];
+      json_result["status"]=json_stringt("failed");
+      jsont &json_trace=json_result["trace"];
       convert(ns, goto_trace, json_trace);
-      status() << preformatted_output << json_result << eom;
+      status() << json_result;
     }
     break;
   }
@@ -173,16 +173,15 @@ void bmct::report_success()
     {
       xmlt xml("cprover-status");
       xml.data="SUCCESS";
-      std::cout << xml;
-      std::cout << "\n";
+      result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("success");
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
@@ -201,16 +200,15 @@ void bmct::report_failure()
     {
       xmlt xml("cprover-status");
       xml.data="FAILURE";
-      std::cout << xml;
-      std::cout << "\n";
+      result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("failure");
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }

src/cbmc/bmc_cover.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "bmc.h"
 
-#include <iostream>
-
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/xml_expr.h>
@@ -185,10 +183,6 @@ void bmc_covert::satisfying_assignment()
       goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
       break;
     }
-
-  #if 0
-  show_goto_trace(std::cout, bmc.ns, test.goto_trace);
-  #endif
 }
 
 bool bmc_covert::operator()()
@@ -223,8 +217,6 @@ bool bmc_covert::operator()()
 
   bmc.do_conversion();
 
-  // bmc.equation.output(std::cout);
-
   // get the conditions for these goals from formula
   // collect all 'instances' of the goals
   for(auto it = bmc.equation.SSA_steps.begin();
@@ -280,26 +272,25 @@ bool bmc_covert::operator()()
   {
     case ui_message_handlert::uit::PLAIN:
     {
-      status() << "\n** coverage results:" << eom;
+      result() << "\n** coverage results:" << eom;
 
       for(const auto &g : goal_map)
       {
         const goalt &goal=g.second;
 
-        status() << "[" << g.first << "]";
+        result() << "[" << g.first << "]";
 
         if(goal.source_location.is_not_nil())
-          status() << ' ' << goal.source_location;
+          result() << ' ' << goal.source_location;
 
         if(!goal.description.empty())
-          status() << ' ' << goal.description;
+          result() << ' ' << goal.description;
 
-        status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
-                 << eom;
+        result() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
+                 << '\n';
       }
 
-      status() << '\n';
-
+      result() << eom;
       break;
     }
 
@@ -317,7 +308,7 @@ bool bmc_covert::operator()()
         if(goal.source_location.is_not_nil())
           xml_result.new_element()=xml(goal.source_location);
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
 
       for(const auto &test : tests)
@@ -350,7 +341,7 @@ bool bmc_covert::operator()()
           xml_goal.set_attribute("id", id2string(goal_id));
         }
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -406,7 +397,8 @@ bool bmc_covert::operator()()
           goal_refs.push_back(json_stringt(id2string(goal_id)));
         }
       }
-      std::cout << ",\n" << json_result;
+
+      result() << json_result;
       break;
     }
   }
@@ -424,10 +416,12 @@ bool bmc_covert::operator()()
 
   if(bmc.ui==ui_message_handlert::uit::PLAIN)
   {
-    std::cout << "Test suite:" << '\n';
+    result() << "Test suite:" << '\n';
 
     for(const auto &test : tests)
-      std::cout << get_test(test.goto_trace) << '\n';
+      result() << get_test(test.goto_trace) << '\n';
+
+    result() << eom;
   }
 
   return false;

src/cbmc/fault_localization.cpp

@@ -301,7 +301,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
       xmlt dest("fault-localization");
       xmlt xml_diagnosis=report_xml(ID_nil);
       dest.new_element().swap(xml_diagnosis);
-      status() << preformatted_output << dest << eom;
+      status() << dest;
       break;
     }
     case ui_message_handlert::uit::JSON_UI:
@@ -379,7 +379,7 @@ void fault_localizationt::report(
         xmlt xml_diagnosis=report_xml(goal_pair.first);
         dest.new_element().swap(xml_diagnosis);
       }
-      status() << preformatted_output << dest << eom;
+      status() << dest;
     }
     break;
   case ui_message_handlert::uit::JSON_UI:

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -564,7 +564,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-natural-loops"))
     {
-      show_natural_loops(goto_model);
+      show_natural_loops(goto_model, std::cout);
       return 0;
     }
 

src/util/cout_message.cpp

@@ -31,10 +31,9 @@ cerr_message_handlert::cerr_message_handlert():
 
 void console_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   if(verbosity<level)
     return;
@@ -102,8 +101,7 @@ void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   const irep_idt file=location.get_file();
   const irep_idt line=location.get_line();
@@ -141,15 +139,14 @@ void gcc_message_handlert::print(
 
   dest+=message;
 
-  print(level, dest, preformatted);
+  print(level, dest);
 }
 
 void gcc_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   // gcc appears to send everything to cerr
   if(verbosity>=level)

src/util/cout_message.h

@@ -32,8 +32,7 @@ class console_message_handlert:public ui_message_handlert
   // level 4 and upwards go to cout, level 1-3 to cerr
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted) override;
+    const std::string &message) override;
 
   virtual void flush(unsigned level) override;
 };
@@ -44,15 +43,13 @@ class gcc_message_handlert:public ui_message_handlert
   // aims to imitate the messages gcc prints
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted) override;
+    const std::string &message) override;
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted) override;
+    const source_locationt &location) override;
 };
 
 #endif // CPROVER_UTIL_COUT_MESSAGE_H