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

@@ -121,9 +121,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);
 
@@ -185,14 +182,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("assumptions", false);
 
   // 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(
@@ -912,17 +904,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.
@@ -966,7 +950,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);
   }
 
@@ -1075,7 +1059,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,12 +380,6 @@ safety_checkert::resultt bmct::execute(
       return safety_checkert::resultt::SAFE; // to indicate non-error
     }
 
-    if(!options.get_list_option("cover").empty())
-    {
-      return cover(goto_functions)?
-        safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
-    }
-
     if(options.get_option("localize-faults")!="")
     {
       fault_localizationt fault_localization(

src/cbmc/bmc.h

@@ -223,12 +223,7 @@ class bmct:public safety_checkert
   void slice();
   void show();
 
-  bool cover(const goto_functionst &goto_functions);
-
   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

@@ -57,7 +57,6 @@ Author: Daniel Kroening, [email protected]
 #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>
 
@@ -151,9 +150,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"));
 
@@ -788,13 +784,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.
@@ -833,7 +822,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);
   }
 
@@ -940,7 +929,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

@@ -62,7 +62,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

@@ -58,7 +58,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) \