diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 6c491f75827..f515a4cbb26 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -93,9 +93,24 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ $(CPROVER_DIR)/src/util/util$(LIBEXT) \ $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \ $(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \ - $(CPROVER_DIR)/src/goto-instrument/goto-instrument$(LIBEXT) \ + $(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_instrument_location$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \ $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ + $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \ $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \ diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 87885153a33..c2bb06a36d0 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -100,7 +100,7 @@ CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) include ../config.inc include ../common -all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) +all: goto-instrument$(EXEEXT) ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) @@ -112,9 +112,6 @@ endif goto-instrument$(EXEEXT): $(OBJ) $(LINKBIN) -goto-instrument$(LIBEXT): $(OBJ) - $(LINKLIB) - .PHONY: goto-instrument-mac-signed goto-instrument-mac-signed: goto-instrument$(EXEEXT) diff --git a/unit/Makefile b/unit/Makefile index eeff4e499fe..09a8fa2939f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -73,6 +73,20 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/symex_bmc$(OBJEXT) \ ../src/cbmc/symex_coverage$(OBJEXT) \ ../src/cbmc/xml_interface$(OBJEXT) \ + ../src/goto-instrument/cover$(OBJEXT) \ + ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \ + ../src/goto-instrument/cover_filter$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_branch$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_condition$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_decision$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_location$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ + ../src/goto-instrument/cover_instrument_other$(OBJEXT) \ + ../src/goto-instrument/cover_util$(OBJEXT) \ + ../src/goto-instrument/reachability_slicer$(OBJEXT) \ + ../src/goto-instrument/nondet_static$(OBJEXT) \ + ../src/goto-instrument/full_slicer$(OBJEXT) \ + ../src/goto-instrument/unwindset$(OBJEXT) \ ../src/xmllang/xmllang$(LIBEXT) \ ../src/goto-symex/goto-symex$(LIBEXT) \ ../src/jsil/jsil$(LIBEXT) \ @@ -85,7 +99,6 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ ../src/util/util$(LIBEXT) \ ../src/big-int/big-int$(LIBEXT) \ ../src/goto-programs/goto-programs$(LIBEXT) \ - ../src/goto-instrument/goto-instrument$(LIBEXT) \ ../src/pointer-analysis/pointer-analysis$(LIBEXT) \ ../src/langapi/langapi$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \