Merge pull request #2875 from tautschnig/no-recursive-lib

Do not build a goto-instrument.a

Author: tautschnig

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

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)

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