summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.am7
-rw-r--r--Makefile.builds.in8
-rw-r--r--src/Makefile.am2
-rw-r--r--src/parser/Makefile.am4
4 files changed, 17 insertions, 4 deletions
diff --git a/Makefile.am b/Makefile.am
index b293da744..f8538b548 100644
--- 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 2eec9c777..44326f0ff 100644
--- 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 199accf85..4244bd053 100644
--- 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 d87db20f5..aca11bbd8 100644
--- 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 \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback