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,19 @@ 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)
+$(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)
 
 
 ###############################################################################

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,23 @@ 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)
+
+$(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)
 
 
 ###############################################################################