Move reporting functions to report_util

Author: peterschrammel

src/cbmc/all_properties.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/report_util.h>
 
 #include <util/xml.h>
 #include <util/json.h>

src/cbmc/bmc.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <linking/static_lifetime_init.h>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/report_util.h>
 #include <goto-checker/solver_factory.h>
 
 #include "counterexample_beautification.h"

src/cbmc/fault_localization.cpp

@@ -27,6 +27,7 @@ Author: Peter Schrammel
 #include <goto-programs/xml_goto_trace.h>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/report_util.h>
 
 #include "counterexample_beautification.h"
 

src/goto-checker/bmc_util.cpp

@@ -225,58 +225,3 @@ void slice(
                    << " remaining after simplification" << messaget::eom;
 }
 
-void report_success(ui_message_handlert &ui_message_handler)
-{
-  messaget msg(ui_message_handler);
-  msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
-
-  switch(ui_message_handler.get_ui())
-  {
-  case ui_message_handlert::uit::PLAIN:
-    break;
-
-  case ui_message_handlert::uit::XML_UI:
-  {
-    xmlt xml("cprover-status");
-    xml.data = "SUCCESS";
-    msg.result() << xml;
-  }
-  break;
-
-  case ui_message_handlert::uit::JSON_UI:
-  {
-    json_objectt json_result;
-    json_result["cProverStatus"] = json_stringt("success");
-    msg.result() << json_result;
-  }
-  break;
-  }
-}
-
-void report_failure(ui_message_handlert &ui_message_handler)
-{
-  messaget msg(ui_message_handler);
-  msg.result() << "VERIFICATION FAILED" << messaget::eom;
-
-  switch(ui_message_handler.get_ui())
-  {
-  case ui_message_handlert::uit::PLAIN:
-    break;
-
-  case ui_message_handlert::uit::XML_UI:
-  {
-    xmlt xml("cprover-status");
-    xml.data = "FAILURE";
-    msg.result() << xml;
-  }
-  break;
-
-  case ui_message_handlert::uit::JSON_UI:
-  {
-    json_objectt json_result;
-    json_result["cProverStatus"] = json_stringt("failure");
-    msg.result() << json_result;
-  }
-  break;
-  }
-}

src/goto-checker/bmc_util.h

@@ -32,9 +32,6 @@ void convert_symex_target_equation(
   prop_convt &,
   message_handlert &);
 
-void report_failure(ui_message_handlert &);
-void report_success(ui_message_handlert &);
-
 void build_error_trace(
   goto_tracet &,
   const namespacet &,

src/goto-checker/report_util.cpp

@@ -13,6 +13,63 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 #include <util/xml.h>
+#include <util/json.h>
+
+void report_success(ui_message_handlert &ui_message_handler)
+{
+  messaget msg(ui_message_handler);
+  msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
+
+  switch(ui_message_handler.get_ui())
+  {
+    case ui_message_handlert::uit::PLAIN:
+      break;
+
+    case ui_message_handlert::uit::XML_UI:
+    {
+      xmlt xml("cprover-status");
+      xml.data = "SUCCESS";
+      msg.result() << xml;
+    }
+      break;
+
+    case ui_message_handlert::uit::JSON_UI:
+    {
+      json_objectt json_result;
+      json_result["cProverStatus"] = json_stringt("success");
+      msg.result() << json_result;
+    }
+      break;
+  }
+}
+
+void report_failure(ui_message_handlert &ui_message_handler)
+{
+  messaget msg(ui_message_handler);
+  msg.result() << "VERIFICATION FAILED" << messaget::eom;
+
+  switch(ui_message_handler.get_ui())
+  {
+    case ui_message_handlert::uit::PLAIN:
+      break;
+
+    case ui_message_handlert::uit::XML_UI:
+    {
+      xmlt xml("cprover-status");
+      xml.data = "FAILURE";
+      msg.result() << xml;
+    }
+      break;
+
+    case ui_message_handlert::uit::JSON_UI:
+    {
+      json_objectt json_result;
+      json_result["cProverStatus"] = json_stringt("failure");
+      msg.result() << json_result;
+    }
+      break;
+  }
+}
 
 void output_properties(
   const propertiest &properties,

src/goto-checker/report_util.h

@@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel
 
 class ui_message_handlert;
 
+void report_success(ui_message_handlert &);
+void report_failure(ui_message_handlert &);
+
 void output_properties(
   const propertiest &properties,
   ui_message_handlert &ui_message_handler);