Use goto verifier for --cover in CBMC

instead of bmc_covert

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/cover_goals_verifier_with_trace_storage.h>
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/multi_path_symex_only_checker.h>
 #include <goto-checker/properties.h>
@@ -72,6 +73,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
+#include "c_test_input_generator.h"
 #include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
@@ -570,6 +572,19 @@ int cbmc_parse_optionst::doit()
     }
   }
 
+  if(options.is_set("cover"))
+  {
+    cover_goals_verifier_with_trace_storaget<multi_path_symex_checkert>
+      verifier(options, ui_message_handler, goto_model);
+    (void)verifier();
+    verifier.report();
+
+    c_test_input_generatort test_generator(ui_message_handler, options);
+    test_generator(verifier.get_traces());
+
+    return CPROVER_EXIT_SUCCESS;
+  }
+
   std::unique_ptr<goto_verifiert> verifier = nullptr;
 
   if(
@@ -599,6 +614,7 @@ int cbmc_parse_optionst::doit()
 
   resultt result = (*verifier)();
   verifier->report();
+
   return result_to_exit_code(result);
 }