Make bmct::report_{success,failure} static

This is in preparation for a future commit, where the static method
do_language_agnostic_bmc will need to make a final report after all
paths have been exhausted.

These methods were previously marked as virtual, so the zero-parameter
non-static variants of these methods have been kept as a convenience;
they do nothing other than call into the static variant.

Author: karkhaz

src/cbmc/bmc.cpp

@@ -153,9 +153,14 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
 
 void bmct::report_success()
 {
-  result() << bold << "VERIFICATION SUCCESSFUL" << reset << eom;
+  report_success(*this, ui_message_handler);
+}
 
-  switch(ui_message_handler.get_ui())
+void bmct::report_success(messaget &log, ui_message_handlert &handler)
+{
+  log.result() << log.bold << "VERIFICATION SUCCESSFUL" << log.reset << log.eom;
+
+  switch(handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -164,25 +169,30 @@ void bmct::report_success()
     {
       xmlt xml("cprover-status");
       xml.data="SUCCESS";
-      result() << xml;
+      log.result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("success");
-      result() << json_result;
+      log.result() << json_result;
     }
     break;
   }
 }
 
 void bmct::report_failure()
 {
-  result() << bold << "VERIFICATION FAILED" << reset << eom;
+  report_failure(*this, ui_message_handler);
+}
 
-  switch(ui_message_handler.get_ui())
+void bmct::report_failure(messaget &log, ui_message_handlert &handler)
+{
+  log.result() << log.bold << "VERIFICATION FAILED" << log.reset << log.eom;
+
+  switch(handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -191,15 +201,15 @@ void bmct::report_failure()
     {
       xmlt xml("cprover-status");
       xml.data="FAILURE";
-      result() << xml;
+      log.result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("failure");
-      result() << json_result;
+      log.result() << json_result;
     }
     break;
   }

src/cbmc/bmc.h

@@ -208,6 +208,9 @@ class bmct:public safety_checkert
   virtual void report_success();
   virtual void report_failure();
 
+  static void report_success(messaget &, ui_message_handlert &);
+  static void report_failure(messaget &, ui_message_handlert &);
+
   virtual void error_trace();
   void output_graphml(resultt result);