Use goto verifier for --cover in CBMC

instead of bmc_covert

Fixes --cover tests without property descriptions.
The unified property handling introduced in a1100e1
used by goto verifier does not allow properties
without description.

Author: peterschrammel

regression/cbmc-cover/assertion1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover assertion
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 9 function main: SATISFIED$
-^\[main.coverage.2\] file main.c line 13 function main: SATISFIED$
+^\[main.coverage.1\] file main.c line 9 function main assertion: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main assertion: SATISFIED$
 --
 ^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -36,6 +36,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>
@@ -73,6 +74,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)
@@ -578,6 +580,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(
@@ -607,6 +622,7 @@ int cbmc_parse_optionst::doit()
 
   resultt result = (*verifier)();
   verifier->report();
+
   return result_to_exit_code(result);
 }