Factor out output_coverage_report into bmc_util

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -276,3 +276,19 @@ void update_properties_status_not_checked(
     }
   }
 }
+
+void output_coverage_report(
+  const std::string &cov_out,
+  const abstract_goto_modelt &goto_model,
+  const symex_bmct &symex,
+  ui_message_handlert &ui_message_handler)
+{
+  if(
+    !cov_out.empty() &&
+    symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
+  {
+    messaget log(ui_message_handler);
+    log.error() << "Failed to write symex coverage report to '" << cov_out
+                << "'" << messaget::eom;
+  }
+}

src/goto-checker/bmc_util.h

@@ -69,6 +69,12 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
+void output_coverage_report(
+  const std::string &cov_out,
+  const abstract_goto_modelt &goto_model,
+  const symex_bmct &symex,
+  ui_message_handlert &ui_message_handler);
+
 /// Sets property status to PASS for properties whose
 /// conditions are constant true in the \p equation.
 /// \param [inout] properties: The status is updated in this data structure

src/goto-checker/multi_path_symex_checker.cpp

@@ -40,7 +40,13 @@ operator()(propertiest &properties)
   if(!symex_has_run)
   {
     perform_symex();
-    output_coverage_report();
+
+    output_coverage_report(
+      options.get_option("symex-coverage-report"),
+      goto_model,
+      symex,
+      ui_message_handler);
+
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, equation);
     // Since we will not symex any further we can decide the status

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -41,7 +41,11 @@ operator()(propertiest &properties)
 {
   perform_symex();
 
-  output_coverage_report();
+  output_coverage_report(
+    options.get_option("symex-coverage-report"),
+    goto_model,
+    symex,
+    ui_message_handler);
 
   if(options.get_bool_option("show-vcc"))
   {
@@ -95,15 +99,3 @@ void multi_path_symex_only_checkert::perform_symex()
     symex.validate(validation_modet::INVARIANT);
   }
 }
-
-void multi_path_symex_only_checkert::output_coverage_report()
-{
-  std::string cov_out = options.get_option("symex-coverage-report");
-  if(
-    !cov_out.empty() &&
-    symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
-  {
-    log.error() << "Failed to write symex coverage report to '" << cov_out
-                << "'" << messaget::eom;
-  }
-}

src/goto-checker/multi_path_symex_only_checker.h

@@ -35,7 +35,6 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
   symex_bmct symex;
 
   void perform_symex();
-  void output_coverage_report();
 };
 
 #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H