From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 24 Sep 2011 18:04:08 +0000 (+0000)
Subject: Fix to building and linking for unit tests.  (This should fix the segfaulting units... 
X-Git-Tag: cvc5-1.0.0~8459
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b79e8b369649f053ce3a39d3d178e4e2dbcf9993;p=cvc5.git

Fix to building and linking for unit tests.  (This should fix the segfaulting units in optimized-dynamic.  The problem was that the code incorrectly determined the address of one of the thread-scoped global variables, and I think it's because the same library was linked twice into the unit test in two different ways, confusing the runtime support code.)
---

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 \