split out ccover from cbmc

Author: Daniel Kroening

.gitignore

@@ -95,6 +95,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

@@ -51,6 +51,8 @@ set_target_properties(
     big-int
     cbmc
     cbmc-lib
+    ccover
+    ccover-lib
     clobber
     clobber-lib
     cpp

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

regression/cbmc/pointer-function-parameters-2/main.c renamed to regression/ccover/pointer-function-parameters-2/main.c

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

regression/cbmc/pointer-function-parameters-2/test.desc renamed to regression/ccover/pointer-function-parameters-2/test.desc

@@ -3,6 +3,7 @@ DIRS = analyses \
        assembler \
        big-int \
        cbmc \
+       ccover \
        clobber \
        cpp \
        goto-analyzer \
@@ -23,6 +24,7 @@ DIRS = analyses \
        # Empty last line
 
 all: cbmc.dir \
+     ccover.dir \
      goto-analyzer.dir \
      goto-cc.dir \
      goto-diff.dir \
@@ -55,6 +57,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
 

regression/cbmc/pointer-function-parameters/main.c renamed to regression/ccover/pointer-function-parameters/main.c

@@ -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)

regression/cbmc/pointer-function-parameters/test.desc renamed to regression/ccover/pointer-function-parameters/test.desc

@@ -0,0 +1,77 @@
+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) \
+       ../java_bytecode/java_bytecode$(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)

regression/cbmc/reachability-slice/test.c renamed to regression/ccover/reachability-slice/test.c

@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Test-Suite Generation with BMC
 
-#include "bmc.h"
+#include "ccover_bmc.h"
 
 #include <chrono>
 #include <iomanip>
@@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
-#include "bv_cbmc.h"
+#include <cbmc/bv_cbmc.h>
 
 class bmc_covert:
   public cover_goalst::observert,
@@ -38,7 +38,7 @@ class bmc_covert:
 public:
   bmc_covert(
     const goto_functionst &_goto_functions,
-    bmct &_bmc):
+    ccover_bmct &_bmc):
     goto_functions(_goto_functions), solver(_bmc.prop_conv), bmc(_bmc)
   {
   }
@@ -141,7 +141,7 @@ class bmc_covert:
 protected:
   const goto_functionst &goto_functions;
   prop_convt &solver;
-  bmct &bmc;
+  ccover_bmct &bmc;
 };
 
 void bmc_covert::satisfying_assignment()
@@ -426,7 +426,7 @@ bool bmc_covert::operator()()
 }
 
 /// Try to cover all goals
-bool bmct::cover(
+bool ccover_bmct::cover(
   const goto_functionst &goto_functions,
   const optionst::value_listt &criteria)
 {