From 04c345a4debffaa82bd3e360aaf7cb4c6f135ed7 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 27 Jan 2010 22:12:33 +0000 Subject: [PATCH] test framework fixes; bug 13 closed --- test/regress/Makefile.am | 1 - test/system/Makefile.am | 31 ++++++++++++++++++++++++++----- test/system/Makefile.in | 31 ++++++++++++++++++++++++++----- test/unit/Makefile.am | 34 ++++++++++++++++++++++++---------- test/unit/Makefile.in | 34 +++++++++++++++++++++++++--------- test/unit/Makefile.tests | 3 +++ 6 files changed, 104 insertions(+), 30 deletions(-) create mode 100644 test/unit/Makefile.tests diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index ba7fd1309..c59885975 100644 --- 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 61527e4d8..a12adc56b 100644 --- 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 4b457a954..2496a1849 100644 --- 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 fcaa2cc5d..f2fb9be92 100644 --- 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 49912b26c..948663478 100644 --- 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 index 000000000..fcd748d0d --- /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)) -- 2.30.2