Replace cout in show_properties

All output should be printed to message streams

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -534,7 +534,8 @@ int cbmc_parse_optionst::doit()
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
-    show_properties(goto_model, ui_message_handler.get_ui());
+    show_properties(
+      goto_model, get_message_handler(), ui_message_handler.get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 

src/clobber/clobber_parse_options.cpp

@@ -150,7 +150,7 @@ int clobber_parse_optionst::doit()
 
     if(cmdline.isset("show-properties"))
     {
-      show_properties(goto_model, get_ui());
+      show_properties(goto_model, get_message_handler(), get_ui());
       return 0;
     }
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -592,7 +592,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, get_ui());
+    show_properties(goto_model, get_message_handler(), get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -532,7 +532,7 @@ int goto_instrument_parse_optionst::doit()
        cmdline.isset("show-properties"))
     {
       const namespacet ns(goto_model.symbol_table);
-      show_properties(goto_model, get_ui());
+      show_properties(goto_model, get_message_handler(), get_ui());
       return CPROVER_EXIT_SUCCESS;
     }
 

src/goto-programs/show_properties.cpp

@@ -46,13 +46,14 @@ optionalt<source_locationt> find_property(
   return { };
 }
 
-
 void show_properties(
   const namespacet &ns,
   const irep_idt &identifier,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui,
   const goto_programt &goto_program)
 {
+  messaget msg(message_handler);
   for(const auto &ins : goto_program.instructions)
   {
     if(!ins.is_assert())
@@ -83,7 +84,7 @@ void show_properties(
         xml_property.new_element("expression").data=
           from_expr(ns, identifier, ins.guard);
 
-        std::cout << xml_property << '\n';
+        msg.result() << xml_property;
       }
       break;
 
@@ -92,14 +93,13 @@ void show_properties(
       break;
 
     case ui_message_handlert::uit::PLAIN:
-      std::cout << "Property " << property_id << ":\n";
+      msg.result() << "Property " << property_id << ":\n";
 
-      std::cout << "  " << ins.source_location << '\n'
-                << "  " << description << '\n'
-                << "  " << from_expr(ns, identifier, ins.guard)
-                        << '\n';
+      msg.result() << "  " << ins.source_location << '\n'
+                   << "  " << description << '\n'
+                   << "  " << from_expr(ns, identifier, ins.guard) << '\n';
 
-      std::cout << '\n';
+      msg.result() << messaget::eom;
       break;
 
     default:
@@ -147,8 +147,10 @@ void show_properties_json(
 
 void show_properties_json(
   const namespacet &ns,
+  message_handlert &message_handler,
   const goto_functionst &goto_functions)
 {
+  messaget msg(message_handler);
   json_arrayt json_properties;
 
   for(const auto &fct : goto_functions.function_map)
@@ -161,29 +163,31 @@ void show_properties_json(
 
   json_objectt json_result;
   json_result["properties"] = json_properties;
-  std::cout << ",\n" << json_result;
+  msg.result() << json_result;
 }
 
 void show_properties(
   const namespacet &ns,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui,
   const goto_functionst &goto_functions)
 {
   if(ui == ui_message_handlert::uit::JSON_UI)
-    show_properties_json(ns, goto_functions);
+    show_properties_json(ns, message_handler, goto_functions);
   else
     for(const auto &fct : goto_functions.function_map)
       if(!fct.second.is_inlined())
-        show_properties(ns, fct.first, ui, fct.second.body);
+        show_properties(ns, fct.first, message_handler, ui, fct.second.body);
 }
 
 void show_properties(
   const goto_modelt &goto_model,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui)
 {
   const namespacet ns(goto_model.symbol_table);
   if(ui == ui_message_handlert::uit::JSON_UI)
-    show_properties_json(ns, goto_model.goto_functions);
+    show_properties_json(ns, message_handler, goto_model.goto_functions);
   else
-    show_properties(ns, ui, goto_model.goto_functions);
+    show_properties(ns, message_handler, ui, goto_model.goto_functions);
 }

src/goto-programs/show_properties.h

@@ -19,13 +19,16 @@ class namespacet;
 class goto_modelt;
 class symbol_tablet;
 class goto_functionst;
+class message_handlert;
 
 void show_properties(
   const goto_modelt &,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui);
 
 void show_properties(
   const namespacet &ns,
+  message_handlert &message_handler,
   ui_message_handlert::uit ui,
   const goto_functionst &goto_functions);
 

src/jbmc/jbmc_parse_options.cpp

@@ -484,7 +484,8 @@ int jbmc_parse_optionst::doit()
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, ui_message_handler.get_ui());
+    show_properties(
+      goto_model, get_message_handler(), ui_message_handler.get_ui());
     return 0; // should contemplate EX_OK from sysexits.h
   }