cleanout test suite generation from cbmc

Author: Daniel Kroening

jbmc/src/jbmc/Makefile

@@ -40,7 +40,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -103,9 +103,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("show-vcc"))
     options.set_option("show-vcc", true);
 
-  if(cmdline.isset("cover"))
-    parse_cover_options(cmdline, options);
-
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
   else
@@ -181,14 +178,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("error-label", cmdline.get_values("error-label"));
 
   // generate unwinding assertions
-  if(cmdline.isset("cover"))
-    options.set_option("unwinding-assertions", false);
-  else
-  {
-    options.set_option(
-      "unwinding-assertions",
-      cmdline.isset("unwinding-assertions"));
-  }
+  options.set_option(
+    "unwinding-assertions",
+    cmdline.isset("unwinding-assertions"));
 
   // generate unwinding assumptions otherwise
   options.set_option(
@@ -940,17 +932,9 @@ bool jbmc_parse_optionst::process_goto_functions(
       remove_unused_functions(goto_model, get_message_handler());
     }
 
-    // remove skips such that trivial GOTOs are deleted and not considered
-    // for coverage annotation:
+    // remove skips such that trivial GOTOs are deleted
     remove_skip(goto_model);
 
-    // instrument cover goals
-    if(cmdline.isset("cover"))
-    {
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
-        return true;
-    }
-
     // label the assertions
     // This must be done after adding assertions and
     // before using the argument of the "property" option.
@@ -994,7 +978,7 @@ bool jbmc_parse_optionst::process_goto_functions(
         full_slicer(goto_model);
     }
 
-    // remove any skips introduced since coverage instrumentation
+    // remove any skips
     remove_skip(goto_model);
   }
 
@@ -1108,7 +1092,6 @@ void jbmc_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)

regression/cbmc-cover/Makefile

@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -p -c ../../../src/ccover/ccover
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -p -c ../../../src/ccover/ccover
 
 show:
 	@for dir in *; do \

src/cbmc/Makefile

@@ -1,6 +1,5 @@
 SRC = all_properties.cpp \
       bmc.cpp \
-      bmc_cover.cpp \
       bv_cbmc.cpp \
       cbmc_dimacs.cpp \
       cbmc_languages.cpp \

src/cbmc/bmc.cpp

@@ -380,14 +380,6 @@ safety_checkert::resultt bmct::execute(
       return safety_checkert::resultt::SAFE; // to indicate non-error
     }
 
-    if(!options.get_list_option("cover").empty())
-    {
-      const optionst::value_listt criteria=
-        options.get_list_option("cover");
-      return cover(goto_functions, criteria)?
-        safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
-    }
-
     if(options.get_option("localize-faults")!="")
     {
       fault_localizationt fault_localization(

src/cbmc/bmc.h

@@ -223,14 +223,7 @@ class bmct:public safety_checkert
   void slice();
   void show();
 
-  bool cover(
-    const goto_functionst &goto_functions,
-    const optionst::value_listt &criteria);
-
   friend class bmc_all_propertiest;
-  friend class bmc_covert;
-  template <template <class goalt> class covert>
-  friend class bmc_goal_covert;
   friend class fault_localizationt;
 
 private:

src/cbmc/cbmc_parse_options.cpp

@@ -56,7 +56,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
-#include <goto-instrument/cover.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -148,9 +147,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("show-vcc"))
     options.set_option("show-vcc", true);
 
-  if(cmdline.isset("cover"))
-    parse_cover_options(cmdline, options);
-
   if(cmdline.isset("mm"))
     options.set_option("mm", cmdline.get_value("mm"));
 
@@ -786,13 +782,6 @@ bool cbmc_parse_optionst::process_goto_program(
     // for coverage annotation:
     remove_skip(goto_model);
 
-    // instrument cover goals
-    if(options.is_set("cover"))
-    {
-      if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
-        return true;
-    }
-
     // label the assertions
     // This must be done after adding assertions and
     // before using the argument of the "property" option.
@@ -831,7 +820,7 @@ bool cbmc_parse_optionst::process_goto_program(
         full_slicer(goto_model);
     }
 
-    // remove any skips introduced since coverage instrumentation
+    // remove any skips
     remove_skip(goto_model);
   }
 
@@ -944,7 +933,6 @@ void cbmc_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -63,7 +63,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
-  "(cover):(symex-coverage-report):" \
+  "(symex-coverage-report):" \
   "(mm):" \
   OPT_TIMESTAMP \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \

unit/Makefile

@@ -51,7 +51,6 @@ testing-utils.dir:
 # We need to link bmc.o to the unit test, so here's everything it depends on...
 BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/bmc$(OBJEXT) \
-          ../src/cbmc/bmc_cover$(OBJEXT) \
           ../src/cbmc/bv_cbmc$(OBJEXT) \
           ../src/cbmc/cbmc_dimacs$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \