Fix to building and linking for unit tests. (This should fix the segfaulting units...

diff --git a/Makefile.am b/Makefile.am
index b293da74450aa9f5fd35866a260af4a8ccf9143d..f8538b548b4224a8a898eb565f4f06dba76d71b8 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -10,7 +10,10 @@ SUBDIRS = src test contrib
 .PHONY: units systemtests regress regress0 regress1 regress2 regress3
 systemtests regress regress0 regress1 regress2 regress3: all
        +(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
+# We descend into "src" with the "check" target here to ensure that
+# the test prerequisites are all built.
 units: all
+       (cd src && $(MAKE) $(AM_MAKEFLAGS) check)
        +(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
 
 LCOV = lcov
@@ -29,6 +32,7 @@ if COVERAGE_ENABLED
 # work...)
 lcov: all
        $(LCOV) -z -d .
+       $(MAKE) check -C src
        +$(MAKE) check -C test/unit
        $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info
        $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES)
@@ -40,6 +44,7 @@ lcov: all
 
 lcov-all: all
        $(LCOV) -z -d .
+       $(MAKE) check -C src
        +$(MAKE) check -C test
        $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info
        $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES)
@@ -57,6 +62,8 @@ lcov18: all
                echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \
                echo $(LCOV) -z -d .; \
                $(LCOV) -z -d . || exit 1; \
+               echo $(MAKE) check -C src || exit 1; \
+               $(MAKE) check -C src || exit 1; \
                echo $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \
                $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \
                echo $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \

diff --git a/Makefile.builds.in b/Makefile.builds.in
index 2eec9c777534d411df39c65b1488da82d5ea8537..44326f0ff6808678d28042743ee54f954280e4c7 100644 (file)
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -122,9 +122,15 @@ endif
        test -e lib || ln -sfv ".$(libdir)" lib
        test -e bin || ln -sfv ".$(bindir)" bin
 
-check test units systemtests regress: all
+# The descent into "src" with target "check" is to build check
+# prerequisites (e.g. CHECK_PROGRAMS, CHECK_LTLIBRARIES, ...).
+check test units:
+       (cd $(CURRENT_BUILD)/src && $(MAKE) check)
+       +(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
+systemtests regress:
        +(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
 units%:
+       (cd $(CURRENT_BUILD)/src && $(MAKE) check)
        +(cd $(CURRENT_BUILD)/test && $(MAKE) units TEST_PREFIX=$(subst units:,,$@))
 regress%: all
        +(cd $(CURRENT_BUILD)/test && $(MAKE) $@)

diff --git a/src/Makefile.am b/src/Makefile.am
index 199accf850bdd8a94d5ab767bfb0a9d6d18d10b3..4244bd0532c3f84d688349d76f18f8e6d944e66c 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -21,7 +21,7 @@ SUBDIRS = lib expr util context theory prop smt printer . parser compat bindings
 
 lib_LTLIBRARIES = libcvc4.la
 if HAVE_CXXTESTGEN
-noinst_LTLIBRARIES = libcvc4_noinst.la
+check_LTLIBRARIES = libcvc4_noinst.la
 endif
 
 libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION)

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index d87db20f52145e3391f70465ebbabcaa693b30a5..aca11bbd843d89a486b4822a3ba01c324b0b703b 100644 (file)
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -21,7 +21,7 @@ SUBDIRS = smt smt2 cvc
 
 lib_LTLIBRARIES = libcvc4parser.la
 if HAVE_CXXTESTGEN
-noinst_LTLIBRARIES = libcvc4parser_noinst.la
+check_LTLIBRARIES = libcvc4parser_noinst.la
 endif
 
 libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
@@ -39,7 +39,7 @@ libcvc4parser_noinst_la_LIBADD = \
        @builddir@/smt2/libparsersmt2.la \
        @builddir@/cvc/libparsercvc.la \
        @builddir@/../lib/libreplacements.la \
-       -L@builddir@/.. -lcvc4
+       @builddir@/../libcvc4_noinst.la
 
 libcvc4parser_la_SOURCES = \
        antlr_input.h \