Merge pull request #1349 from peterschrammel/cleanup/use-preformatted-output

peterschrammel · web-flow · commit 0323ed0b9a76 · 2017-09-18T13:38:51.000+01:00
Make message streams accept XML and JSON data
diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
@@ -11,18 +11,18 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
 
 #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';
   }
 }
diff --git a/src/analyses/natural_loops.h b/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
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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;
   }
diff --git a/src/cbmc/bmc.cpp b/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;
   }
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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()()
@@ -221,8 +215,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();
@@ -278,26 +270,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;
     }
 
@@ -315,7 +306,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)
@@ -348,7 +339,7 @@ bool bmc_covert::operator()()
           xml_goal.set_attribute("id", id2string(goal_id));
         }
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -404,7 +395,8 @@ bool bmc_covert::operator()()
           goal_refs.push_back(json_stringt(id2string(goal_id)));
         }
       }
-      std::cout << ",\n" << json_result;
+
+      result() << json_result;
       break;
     }
   }
@@ -422,10 +414,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;
diff --git a/src/cbmc/fault_localization.cpp b/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:
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -554,7 +554,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;
     }
 
diff --git a/src/util/cout_message.cpp b/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)
diff --git a/src/util/cout_message.h b/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
diff --git a/src/util/message.cpp b/src/util/message.cpp
diff --git a/src/util/message.h b/src/util/message.h
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
diff --git a/src/util/ui_message.h b/src/util/ui_message.h

Original file line number	Diff line number	Diff line change
`@@ -11,18 +11,18 @@ Author: Georg Weissenbacher, [email protected]`
`11`	`11`
`12`	`12`	`#include "natural_loops.h"`
`13`	`13`
`14`		`-#include <iostream>`
`15`		`-`
`16`		`-void show_natural_loops(const goto_modelt &goto_model)`
	`14`	`+void show_natural_loops(`
	`15`	`+ const goto_modelt &goto_model,`
	`16`	`+ std::ostream &out)`
`17`	`17`	`{`
`18`	`18`	`forall_goto_functions(it, goto_model.goto_functions)`
`19`	`19`	`{`
`20`		`- std::cout << "*** " << it->first << '\n';`
	`20`	`+ out << "*** " << it->first << '\n';`
`21`	`21`
`22`	`22`	`natural_loopst natural_loops;`
`23`	`23`	`natural_loops(it->second.body);`
`24`		`- natural_loops.output(std::cout);`
	`24`	`+ natural_loops.output(out);`
`25`	`25`
`26`		`- std::cout << '\n';`
	`26`	`+ out << '\n';`
`27`	`27`	`}`
`28`	`28`	`}`
Original file line number	Diff line number	Diff line change
`@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]`
`11`	`11`
`12`	`12`	`#include "all_properties_class.h"`
`13`	`13`
`14`		`-#include <iostream>`
`15`		`-`
`16`	`14`	`#include <util/time_stopping.h>`
`17`	`15`	`#include <util/xml.h>`
`18`	`16`	`#include <util/json.h>`
`@@ -163,10 +161,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`163`	`161`	`{`
`164`	`162`	`case ui_message_handlert::uit::PLAIN:`
`165`	`163`	`{`
`166`		`- status() << "\n** Results:" << eom;`
	`164`	`+ result() << "\n** Results:" << eom;`
`167`	`165`
`168`	`166`	`for(const auto &goal_pair : goal_map)`
`169`		`- status() << "[" << goal_pair.first << "] "`
	`167`	`+ result() << "[" << goal_pair.first << "] "`
`170`	`168`	`<< goal_pair.second.description << ": "`
`171`	`169`	`<< goal_pair.second.status_string()`
`172`	`170`	`<< eom;`
`@@ -176,10 +174,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`176`	`174`	`for(const auto &g : goal_map)`
`177`	`175`	`if(g.second.status==goalt::statust::FAILURE)`
`178`	`176`	`{`
`179`		`- std::cout << "\n" << "Trace for " << g.first << ":" << "\n";`
`180`		`- show_goto_trace(std::cout, bmc.ns, g.second.goto_trace);`
	`177`	`+ result() << "\n" << "Trace for " << g.first << ":" << "\n";`
	`178`	`+ show_goto_trace(result(), bmc.ns, g.second.goto_trace);`
`181`	`179`	`}`
`182`	`180`	`}`
	`181`	`+ result() << eom;`
`183`	`182`
`184`	`183`	`status() << "\n** " << cover_goals.number_covered()`
`185`	`184`	`<< " of " << cover_goals.size() << " failed ("`
`@@ -200,7 +199,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`200`	`199`	`if(g.second.status==goalt::statust::FAILURE)`
`201`	`200`	`convert(bmc.ns, g.second.goto_trace, xml_result.new_element());`
`202`	`201`
`203`		`- std::cout << xml_result << "\n";`
	`202`	`+ result() << xml_result;`
`204`	`203`	`}`
`205`	`204`	`break;`
`206`	`205`	`}`
`@@ -224,7 +223,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`224`	`223`	`}`
`225`	`224`	`}`
`226`	`225`
`227`		`- std::cout << ",\n" << json_result;`
	`226`	`+ result() << json_result;`
`228`	`227`	`}`
`229`	`228`	`break;`
`230`	`229`	`}`
Original file line number	Diff line number	Diff line change
`@@ -55,33 +55,33 @@ void bmct::error_trace()`
`55`	`55`	`switch(ui)`
`56`	`56`	`{`
`57`	`57`	`case ui_message_handlert::uit::PLAIN:`
`58`		`- status() << "Counterexample:" << eom;`
`59`		`- show_goto_trace(status(), ns, goto_trace);`
`60`		`- status() << eom;`
	`58`	`+ result() << "Counterexample:" << eom;`
	`59`	`+ show_goto_trace(result(), ns, goto_trace);`
	`60`	`+ result() << eom;`
`61`	`61`	`break;`
`62`	`62`
`63`	`63`	`case ui_message_handlert::uit::XML_UI:`
`64`	`64`	`{`
`65`	`65`	`xmlt xml;`
`66`	`66`	`convert(ns, goto_trace, xml);`
`67`		`- status() << preformatted_output << xml << eom;`
	`67`	`+ status() << xml;`
`68`	`68`	`}`
`69`	`69`	`break;`
`70`	`70`
`71`	`71`	`case ui_message_handlert::uit::JSON_UI:`
`72`	`72`	`{`
`73`		`- json_objectt json_result;`
`74`		`- json_arrayt &result_array=json_result["results"].make_array();`
`75`		`- json_objectt &result=result_array.push_back().make_object();`
	`73`	`+ json_objectt json;`
	`74`	`+ json_arrayt &result_array=json["results"].make_array();`
	`75`	`+ json_objectt &json_result=result_array.push_back().make_object();`
`76`	`76`	`const goto_trace_stept &step=goto_trace.steps.back();`
`77`		`- result["property"]=`
	`77`	`+ json_result["property"]=`
`78`	`78`	`json_stringt(id2string(step.pc->source_location.get_property_id()));`
`79`		`- result["description"]=`
	`79`	`+ json_result["description"]=`
`80`	`80`	`json_stringt(id2string(step.pc->source_location.get_comment()));`
`81`		`- result["status"]=json_stringt("failed");`
`82`		`- jsont &json_trace=result["trace"];`
	`81`	`+ json_result["status"]=json_stringt("failed");`
	`82`	`+ jsont &json_trace=json_result["trace"];`
`83`	`83`	`convert(ns, goto_trace, json_trace);`
`84`		`- status() << preformatted_output << json_result << eom;`
	`84`	`+ status() << json_result;`
`85`	`85`	`}`
`86`	`86`	`break;`
`87`	`87`	`}`
`@@ -173,16 +173,15 @@ void bmct::report_success()`
`173`	`173`	`{`
`174`	`174`	`xmlt xml("cprover-status");`
`175`	`175`	`xml.data="SUCCESS";`
`176`		`- std::cout << xml;`
`177`		`- std::cout << "\n";`
	`176`	`+ result() << xml;`
`178`	`177`	`}`
`179`	`178`	`break;`
`180`	`179`
`181`	`180`	`case ui_message_handlert::uit::JSON_UI:`
`182`	`181`	`{`
`183`	`182`	`json_objectt json_result;`
`184`	`183`	`json_result["cProverStatus"]=json_stringt("success");`
`185`		`- std::cout << ",\n" << json_result;`
	`184`	`+ result() << json_result;`
`186`	`185`	`}`
`187`	`186`	`break;`
`188`	`187`	`}`
`@@ -201,16 +200,15 @@ void bmct::report_failure()`
`201`	`200`	`{`
`202`	`201`	`xmlt xml("cprover-status");`
`203`	`202`	`xml.data="FAILURE";`
`204`		`- std::cout << xml;`
`205`		`- std::cout << "\n";`
	`203`	`+ result() << xml;`
`206`	`204`	`}`
`207`	`205`	`break;`
`208`	`206`
`209`	`207`	`case ui_message_handlert::uit::JSON_UI:`
`210`	`208`	`{`
`211`	`209`	`json_objectt json_result;`
`212`	`210`	`json_result["cProverStatus"]=json_stringt("failure");`
`213`		`- std::cout << ",\n" << json_result;`
	`211`	`+ result() << json_result;`
`214`	`212`	`}`
`215`	`213`	`break;`
`216`	`214`	`}`
Original file line number	Diff line number	Diff line change
`@@ -301,7 +301,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()`
`301`	`301`	`xmlt dest("fault-localization");`
`302`	`302`	`xmlt xml_diagnosis=report_xml(ID_nil);`
`303`	`303`	`dest.new_element().swap(xml_diagnosis);`
`304`		`- status() << preformatted_output << dest << eom;`
	`304`	`+ status() << dest;`
`305`	`305`	`break;`
`306`	`306`	`}`
`307`	`307`	`case ui_message_handlert::uit::JSON_UI:`
`@@ -379,7 +379,7 @@ void fault_localizationt::report(`
`379`	`379`	`xmlt xml_diagnosis=report_xml(goal_pair.first);`
`380`	`380`	`dest.new_element().swap(xml_diagnosis);`
`381`	`381`	`}`
`382`		`- status() << preformatted_output << dest << eom;`
	`382`	`+ status() << dest;`
`383`	`383`	`}`
`384`	`384`	`break;`
`385`	`385`	`case ui_message_handlert::uit::JSON_UI:`
Original file line number	Diff line number	Diff line change
`@@ -554,7 +554,7 @@ int goto_instrument_parse_optionst::doit()`
`554`	`554`
`555`	`555`	`if(cmdline.isset("show-natural-loops"))`
`556`	`556`	`{`
`557`		`- show_natural_loops(goto_model);`
	`557`	`+ show_natural_loops(goto_model, std::cout);`
`558`	`558`	`return 0;`
`559`	`559`	`}`
`560`	`560`