Merge pull request #2847 from peterschrammel/jbmc-no-cover

Remove --cover option from JBMC

Author: peterschrammel

jbmc/regression/CMakeLists.txt

@@ -10,5 +10,4 @@ add_subdirectory(jdiff)
 add_subdirectory(janalyzer-taint)
 add_subdirectory(jbmc-concurrency)
 add_subdirectory(jbmc-inheritance)
-add_subdirectory(jbmc-cover)
 add_subdirectory(jbmc-generics)

jbmc/regression/Makefile

@@ -4,7 +4,6 @@
 DIRS = janalyzer-taint \
        jbmc \
        jbmc-concurrency \
-       jbmc-cover \
        jbmc-inheritance \
        jbmc-strings \
        jdiff \

jbmc/regression/jbmc-cover/CMakeLists.txt

@@ -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("nondet-static"))
     options.set_option("nondet-static", true);
 
@@ -189,14 +186,8 @@ 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"));
-  }
+  if(cmdline.isset("unwinding-assertions"))
+    options.set_option("unwinding-assertions", true);
 
   // generate unwinding assumptions otherwise
   options.set_option(
@@ -559,12 +550,6 @@ int jbmc_parse_optionst::doit()
     // particular function:
     add_failed_symbols(lazy_goto_model.symbol_table);
 
-    // If applicable, parse the coverage instrumentation configuration, which
-    // will be used in process_goto_function:
-    cover_config =
-      get_cover_config(
-        options, lazy_goto_model.symbol_table, get_message_handler());
-
     // Provide show-goto-functions and similar dump functions after symex
     // executes. If --paths is active, these dump routines run after every
     // paths iteration. Its return value indicates that if we ran any dump
@@ -782,20 +767,12 @@ void jbmc_parse_optionst::process_goto_function(
         symbol_table);
     }
 
-    // If using symex-driven function loading we must insert the coverage goals
+    // If using symex-driven function loading we must label the assertions
     // now so symex sees its targets; otherwise we leave this until
     // process_goto_functions, as we haven't run remove_exceptions yet, and that
     // pass alters the CFG.
     if(using_symex_driven_loading)
     {
-      // instrument cover goals
-      if(cmdline.isset("cover"))
-      {
-        INVARIANT(
-          cover_config != nullptr, "cover config should have been parsed");
-        instrument_cover_goals(*cover_config, function, get_message_handler());
-      }
-
       // label the assertions
       label_properties(goto_function.body);
 
@@ -916,17 +893,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.
@@ -970,7 +939,7 @@ bool jbmc_parse_optionst::process_goto_functions(
         full_slicer(goto_model);
     }
 
-    // remove any skips introduced since coverage instrumentation
+    // remove any skips introduced
     remove_skip(goto_model);
   }
 
@@ -1079,7 +1048,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(*)

jbmc/regression/jbmc-cover/Makefile

@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <cbmc/bmc.h>
 
-#include <goto-instrument/cover.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_trace.h>
 #include <goto-programs/lazy_goto_model.h>
@@ -69,7 +68,7 @@ class optionst;
   "(verbosity):" \
   "(nondet-static)" \
   "(version)" \
-  "(cover):(symex-coverage-report):" \
+  "(symex-coverage-report):" \
   OPT_TIMESTAMP \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \
   "(ppc-macos)" \
@@ -120,7 +119,6 @@ class jbmc_parse_optionst:
 
 protected:
   ui_message_handlert ui_message_handler;
-  std::unique_ptr<cover_configt> cover_config;
   path_strategy_choosert path_strategy_chooser;
   object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;