Cleanup dependencies in unit test builds, check number of tests

Author: tautschnig

jbmc/unit/Makefile

@@ -1,4 +1,4 @@
-.PHONY: all cprover.dir jprover.dir testing-utils.dir java-testing-utils.dir test
+.PHONY: all jprover.dir test
 
 # Source files for test utilities
 SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \
@@ -64,16 +64,13 @@ include ../src/config.inc
 include $(CPROVER_DIR)/src/config.inc
 include $(CPROVER_DIR)/src/common
 
-cprover.dir:
-	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src
-
 jprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src
 
-cprover-testing-utils.dir:
+$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT): jprover.dir
 	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils
 
-java-testing-utils.dir:
+java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir
 	$(MAKE) $(MAKEARGS) -C java-testing-utils
 
 # We need to link bmc.o to the unit test, so here's everything it depends on...
@@ -126,16 +123,21 @@ OBJ += $(CPROVER_LIBS) \
        $(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \
        java-testing-utils/java-testing-utils$(LIBEXT)
 
-TESTS = unit_tests$(EXEEXT) \
-        # Empty last line
+CATCH_TEST = unit_tests$(EXEEXT)
+N_CATCH_TESTS = 84
+
+CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT)
 
-CLEANFILES = $(TESTS)
+# only add a dependency for libraries to avoid triggering implicit rules, which
+# would cause unnecessary rebuilds
+$(filter %$(LIBEXT), CPROVER_LIBS): jprover.dir
 
-all: cprover.dir cprover-testing-utils.dir jprover.dir java-testing-utils.dir
-	$(MAKE) $(MAKEARGS) $(TESTS)
+all: $(CATCH_TEST)
 
-test: all
-	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
+test: $(CATCH_TEST)
+	if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases$$" ; then \
+	  ./$(CATCH_TEST) -l ; fi
+	./$(CATCH_TEST)
 
 
 ###############################################################################

src/ansi-c/Makefile

@@ -115,8 +115,6 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c
 %.inc: %.h file_converter$(EXEEXT)
 	./file_converter$(EXEEXT) < $< > $@
 
-cprover_library.cpp: cprover_library.inc
-
 ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES)
 
 generated_files: \

src/cpp/Makefile

@@ -59,6 +59,11 @@ all: cpp$(LIBEXT)
 
 ###############################################################################
 
+# extra dependencies
+cprover_library$(OBJEXT): cprover_library.inc
+
+###############################################################################
+
 ../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp
 	$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
 
@@ -69,8 +74,6 @@ library_check: library/*.c
 cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c
 	cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@
 
-cprover_library.cpp: cprover_library.inc
-
 generated_files: cprover_library.inc
 
 ###############################################################################

unit/Makefile

@@ -1,4 +1,4 @@
-.PHONY: all cprover.dir testing-utils.dir test
+.PHONY: all cprover.dir test
 
 # Source files for test utilities
 SRC = unit_tests.cpp \
@@ -56,7 +56,7 @@ include ../src/common
 cprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src
 
-testing-utils.dir:
+testing-utils/testing-utils$(LIBEXT): cprover.dir
 	$(MAKE) $(MAKEARGS) -C testing-utils
 
 # We need to link bmc.o to the unit test, so here's everything it depends on...
@@ -97,17 +97,25 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \
 
 OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT)
 
-TESTS = unit_tests$(EXEEXT) \
-        miniBDD$(EXEEXT) \
+CATCH_TEST = unit_tests$(EXEEXT)
+N_CATCH_TESTS = 62
+
+TESTS = miniBDD$(EXEEXT) \
         # Empty last line
 
-CLEANFILES = $(TESTS)
+CLEANFILES = $(CATCH_TEST) $(TESTS) testing-utils/testing-utils$(LIBEXT)
+
+# only add a dependency for libraries to avoid triggering implicit rules, which
+# would cause unnecessary rebuilds
+$(filter %$(LIBEXT), CPROVER_LIBS): cprover.dir
 
-all: cprover.dir testing-utils.dir
-	$(MAKE) $(MAKEARGS) $(TESTS)
+all: $(CATCH_TEST) $(TESTS)
 
-test: all
+test: $(CATCH_TEST) $(TESTS)
 	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
+	if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases$$" ; then \
+		./$(CATCH_TEST) -l ; fi
+	./$(CATCH_TEST)
 
 
 ###############################################################################