split test suite generation out of cbmc/jbmc

.gitignore

@@ -96,6 +96,8 @@ src/memory-models/mm_y.tab.h
 # binaries
 src/cbmc/cbmc
 src/cbmc/cbmc.exe
+src/ccover/ccover
+src/ccover/ccover.exe
 src/goto-analyzer/goto-analyzer
 src/goto-analyzer/goto-analyzer.exe
 src/goto-cc/goto-cc

CMakeLists.txt

@@ -52,6 +52,8 @@ set_target_properties(
     big-int
     cbmc
     cbmc-lib
+    ccover
+    ccover-lib
     cpp
     driver
     goto-analyzer

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("nondet-static"))
     options.set_option("nondet-static", true);
 
@@ -189,14 +186,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(
@@ -916,17 +908,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 +954,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);
   }
 
@@ -1079,7 +1063,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 \

regression/ccover/Makefile

@@ -0,0 +1,19 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/ccover/ccover -X smt-backend
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/ccover/ccover -X smt-backend
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

src/CMakeLists.txt

@@ -97,6 +97,7 @@ add_subdirectory(util)
 add_subdirectory(xmllang)
 
 add_subdirectory(cbmc)
+add_subdirectory(ccover)
 add_subdirectory(goto-cc)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)

src/Makefile

@@ -3,6 +3,7 @@ DIRS = analyses \
        assembler \
        big-int \
        cbmc \
+       ccover \
        cpp \
        goto-analyzer \
        goto-cc \
@@ -21,6 +22,7 @@ DIRS = analyses \
        # Empty last line
 
 all: cbmc.dir \
+     ccover.dir \
      goto-analyzer.dir \
      goto-cc.dir \
      goto-diff.dir \
@@ -53,6 +55,8 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
           goto-instrument.dir
 
+ccover.dir: cbmc.dir
+
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir
 

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, 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>
 
@@ -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"));
 
@@ -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);
   }
 
@@ -937,7 +926,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)" \

src/ccover/CMakeLists.txt

@@ -0,0 +1,35 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/ccover_main.cpp
+)
+add_library(ccover-lib ${sources})
+
+generic_includes(ccover-lib)
+
+target_link_libraries(ccover-lib
+    analyses
+    ansi-c
+    assembler
+    big-int
+    cbmc-lib
+    cpp
+    goto-instrument-lib
+    goto-programs
+    goto-symex
+    java_bytecode
+    json
+    langapi
+    linking
+    pointer-analysis
+    solvers
+    util
+    xml
+)
+
+add_if_library(ccover-lib bv_refinement)
+add_if_library(ccover-lib jsil)
+
+# Executable
+add_executable(ccover ccover_main.cpp)
+target_link_libraries(ccover ccover-lib)

src/ccover/Makefile

@@ -0,0 +1,76 @@
+SRC = ccover_bmc.cpp \
+      bmc_cover.cpp \
+      ccover_main.cpp \
+      ccover_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+       ../cpp/cpp$(LIBEXT) \
+       ../linking/linking$(LIBEXT) \
+       ../big-int/big-int$(LIBEXT) \
+       ../goto-programs/goto-programs$(LIBEXT) \
+       ../goto-symex/goto-symex$(LIBEXT) \
+       ../pointer-analysis/value_set$(OBJEXT) \
+       ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \
+       ../pointer-analysis/value_set_domain_fi$(OBJEXT) \
+       ../pointer-analysis/value_set_fi$(OBJEXT) \
+       ../pointer-analysis/value_set_dereference$(OBJEXT) \
+       ../pointer-analysis/dereference_callback$(OBJEXT) \
+       ../pointer-analysis/add_failed_symbols$(OBJEXT) \
+       ../pointer-analysis/rewrite_index$(OBJEXT) \
+       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+       ../goto-instrument/full_slicer$(OBJEXT) \
+       ../goto-instrument/nondet_static$(OBJEXT) \
+       ../goto-instrument/cover$(OBJEXT) \
+       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
+       ../goto-instrument/cover_filter$(OBJEXT) \
+       ../goto-instrument/cover_instrument_branch$(OBJEXT) \
+       ../goto-instrument/cover_instrument_condition$(OBJEXT) \
+       ../goto-instrument/cover_instrument_decision$(OBJEXT) \
+       ../goto-instrument/cover_instrument_location$(OBJEXT) \
+       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+       ../goto-instrument/cover_instrument_other$(OBJEXT) \
+       ../goto-instrument/cover_util$(OBJEXT) \
+       ../goto-instrument/unwindset$(OBJEXT) \
+       ../analyses/analyses$(LIBEXT) \
+       ../langapi/langapi$(LIBEXT) \
+       ../xmllang/xmllang$(LIBEXT) \
+       ../assembler/assembler$(LIBEXT) \
+       ../solvers/solvers$(LIBEXT) \
+       ../util/util$(LIBEXT) \
+       ../json/json$(LIBEXT) \
+       ../cbmc/bv_cbmc$(OBJEXT) \
+       ../cbmc/cbmc_dimacs$(OBJEXT) \
+       ../cbmc/cbmc_solvers$(OBJEXT) \
+       ../cbmc/symex_bmc$(OBJEXT)
+
+INCLUDES= -I ..
+
+LIBS =
+
+include ../config.inc
+include ../common
+
+CLEANFILES = ccover$(EXEEXT)
+
+all: ccover$(EXEEXT)
+
+ifneq ($(wildcard ../bv_refinement/Makefile),)
+  OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
+endif
+
+ifneq ($(wildcard ../jsil/Makefile),)
+  OBJ += ../jsil/jsil$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_JSIL
+endif
+
+###############################################################################
+
+ccover$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: ccover-mac-signed
+
+ccover-mac-signed: ccover$(EXEEXT)
+	strip ccover$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) ccover$(EXEEXT)