test framework fixes; bug 13 closed

diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index ba7fd1309c13c341ab6e3c1b199cd681a4dfb630..c59885975109b0aef90a86178deea3989f13eb39 100644 (file)
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -35,4 +35,3 @@ TESTS = \
        wiki.cvc \
        logops.cvc \
        comb2.shuffled-as.sat03-420.smt
-

diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 61527e4d85bc6712cf8f7137e5516308e2d296b4..a12adc56be263abf5d2ce7ce0456a1ce5220e9c5 100644 (file)
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -1,5 +1,26 @@
-TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
-TESTS = \
-       simple.cvc \
-       simple.smt \
-       bug1.cvc
+TESTS_ENVIRONMENT =
+TESTS =
+
+# Things that aren't tests but that tests rely on and need to
+# go into the distribution
+TEST_DEPS_DIST =
+
+# Make-level dependencies; these don't go in the source distribution
+# but should trigger a re-compile of all unit tests.  Libraries are
+# included here because (1) if static-linking, the tests must be
+# relinked, and (2) if they've changed that means the sources changed,
+# and that means we should ensure the tests compile against any
+# changes made in the header files.
+TEST_DEPS_NODIST = \
+       $(abs_top_builddir)/src/libcvc4.la \
+       $(abs_top_builddir)/src/parser/libcvc4parser.la
+
+TEST_DEPS = \
+       $(TEST_DEPS_DIST) \
+       $(TEST_DEPS_NODIST)
+
+EXTRA_DIST = \
+       $(TEST_DEPS_DIST)
+
+# rebuild tests if a library changes
+$(TESTS):: $(TEST_DEPS)

diff --git a/test/system/Makefile.in b/test/system/Makefile.in
index 4b457a954d03fe8341776b5e30ef1e739c4ef7e5..2496a1849d35016cea8586ddada61b2738eba12f 100644 (file)
--- a/test/system/Makefile.in
+++ b/test/system/Makefile.in
@@ -34,6 +34,7 @@ POST_UNINSTALL = :
 build_triplet = @build@
 host_triplet = @host@
 target_triplet = @target@
+TESTS =
 subdir = test/system
 DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
 ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
@@ -192,11 +193,28 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
-TESTS = \
-       simple.cvc \
-       simple.smt \
-       bug1.cvc
+TESTS_ENVIRONMENT = 
+
+# Things that aren't tests but that tests rely on and need to
+# go into the distribution
+TEST_DEPS_DIST = 
+
+# Make-level dependencies; these don't go in the source distribution
+# but should trigger a re-compile of all unit tests.  Libraries are
+# included here because (1) if static-linking, the tests must be
+# relinked, and (2) if they've changed that means the sources changed,
+# and that means we should ensure the tests compile against any
+# changes made in the header files.
+TEST_DEPS_NODIST = \
+       $(abs_top_builddir)/src/libcvc4.la \
+       $(abs_top_builddir)/src/parser/libcvc4parser.la
+
+TEST_DEPS = \
+       $(TEST_DEPS_DIST) \
+       $(TEST_DEPS_NODIST)
+
+EXTRA_DIST = \
+       $(TEST_DEPS_DIST)
 
 all: all-am
 
@@ -477,6 +495,9 @@ uninstall-am:
        uninstall uninstall-am
 
 
+# rebuild tests if a library changes
+$(TESTS):: $(TEST_DEPS)
+
 # Tell versions [3.59,3.63) of GNU make to not export all variables.
 # Otherwise a system limit (for SysV at least) may be exceeded.
 .NOEXPORT:

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index fcaa2cc5daf2a51966069bc620367e811c948a05..f2fb9be92257a6901b6fc97366086bee97a00593 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,14 +1,28 @@
-# all unit tests
+# All unit tests
 UNIT_TESTS = \
        expr/node_white \
        expr/node_black \
        parser/parser_black
 
-TESTS_DEPENDENCIES = $(abs_top_builddir)/src/libcvc4.la $(abs_top_builddir)/src/parser/libcvc4parser.la
-
-# things that aren't tests but that tests rely on and need to
+# Things that aren't tests but that tests rely on and need to
 # go into the distribution
-TEST_DEPS =
+TEST_DEPS_DIST =
+
+# Make-level dependencies; these don't go in the source distribution
+# but should trigger a re-compile of all unit tests.  Libraries are
+# included here because (1) if static-linking, the tests must be
+# relinked, and (2) if they've changed that means the sources changed,
+# and that means we should ensure the tests compile against any
+# changes made in the header files.
+TEST_DEPS_NODIST = \
+       $(abs_top_builddir)/src/libcvc4.la \
+       $(abs_top_builddir)/src/parser/libcvc4parser.la
+
+TEST_DEPS = \
+       $(TEST_DEPS_DIST) \
+       $(TEST_DEPS_NODIST)
+
+@mk_include@ @srcdir@/Makefile.tests
 
 if HAVE_CXXTESTGEN
 
@@ -34,7 +48,7 @@ TESTS = $(UNIT_TESTS)
 
 EXTRA_DIST = \
        no_cxxtest \
-       $(TEST_DEPS)
+       $(TEST_DEPS_DIST)
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
 noinst_LTLIBRARIES = libdummy.la
@@ -44,13 +58,13 @@ libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 $(TESTS:%=%.cpp): %.cpp: %.h
        mkdir -p `dirname "$@"`
        @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
-$(filter %_white,$(TESTS)): %_white: %_white.cpp
+$(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
        $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
        $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
-$(filter %_black,$(TESTS)): %_black: %_black.cpp
+$(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS)
        $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
        $(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
-$(filter %_public,$(TESTS)): %_public: %_public.cpp
+$(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
        $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
        $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 
@@ -63,6 +77,6 @@ TESTS = no_cxxtest
 
 EXTRA_DIST = \
        $(UNIT_TESTS) \
-       $(TEST_DEPS)
+       $(TEST_DEPS_DIST)
 
 endif

diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index 49912b26c9a759a440087afc53170f31117dabfd..9486634783c0aca0340ed66d57ff550a842dd91c 100644 (file)
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -216,17 +216,31 @@ top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
 
-# all unit tests
+# All unit tests
 UNIT_TESTS = \
        expr/node_white \
        expr/node_black \
        parser/parser_black
 
-TESTS_DEPENDENCIES = $(abs_top_builddir)/src/libcvc4.la $(abs_top_builddir)/src/parser/libcvc4parser.la
 
-# things that aren't tests but that tests rely on and need to
+# Things that aren't tests but that tests rely on and need to
 # go into the distribution
-TEST_DEPS = 
+TEST_DEPS_DIST = 
+
+# Make-level dependencies; these don't go in the source distribution
+# but should trigger a re-compile of all unit tests.  Libraries are
+# included here because (1) if static-linking, the tests must be
+# relinked, and (2) if they've changed that means the sources changed,
+# and that means we should ensure the tests compile against any
+# changes made in the header files.
+TEST_DEPS_NODIST = \
+       $(abs_top_builddir)/src/libcvc4.la \
+       $(abs_top_builddir)/src/parser/libcvc4parser.la
+
+TEST_DEPS = \
+       $(TEST_DEPS_DIST) \
+       $(TEST_DEPS_NODIST)
+
 @HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \
 @HAVE_CXXTESTGEN_TRUE@ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
 @HAVE_CXXTESTGEN_TRUE@ $(TEST_CPPFLAGS)
@@ -253,11 +267,11 @@ TEST_DEPS =
 @HAVE_CXXTESTGEN_TRUE@TESTS = $(UNIT_TESTS)
 @HAVE_CXXTESTGEN_FALSE@EXTRA_DIST = \
 @HAVE_CXXTESTGEN_FALSE@        $(UNIT_TESTS) \
-@HAVE_CXXTESTGEN_FALSE@        $(TEST_DEPS)
+@HAVE_CXXTESTGEN_FALSE@        $(TEST_DEPS_DIST)
 
 @HAVE_CXXTESTGEN_TRUE@EXTRA_DIST = \
 @HAVE_CXXTESTGEN_TRUE@ no_cxxtest \
-@HAVE_CXXTESTGEN_TRUE@ $(TEST_DEPS)
+@HAVE_CXXTESTGEN_TRUE@ $(TEST_DEPS_DIST)
 
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
@@ -646,16 +660,18 @@ uninstall-am:
        tags uninstall uninstall-am
 
 
+@mk_include@ @srcdir@/Makefile.tests
+
 @HAVE_CXXTESTGEN_TRUE@$(TESTS:%=%.cpp): %.cpp: %.h
 @HAVE_CXXTESTGEN_TRUE@ mkdir -p `dirname "$@"`
 @HAVE_CXXTESTGEN_TRUE@ @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
-@HAVE_CXXTESTGEN_TRUE@$(filter %_white,$(TESTS)): %_white: %_white.cpp
+@HAVE_CXXTESTGEN_TRUE@$(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
 @HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
-@HAVE_CXXTESTGEN_TRUE@$(filter %_black,$(TESTS)): %_black: %_black.cpp
+@HAVE_CXXTESTGEN_TRUE@$(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS)
 @HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
-@HAVE_CXXTESTGEN_TRUE@$(filter %_public,$(TESTS)): %_public: %_public.cpp
+@HAVE_CXXTESTGEN_TRUE@$(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
 @HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 

diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests
new file mode 100644 (file)
index 0000000..fcd748d
--- /dev/null
+++ b/test/unit/Makefile.tests
@@ -0,0 +1,3 @@
+WHITE_TESTS = $(filter %_white,$(TESTS))
+BLACK_TESTS = $(filter %_black,$(TESTS))
+PUBLIC_TESTS = $(filter %_public,$(TESTS))