blob: 451100b59a2e079f3111704460199612e76c375f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
# All unit tests
UNIT_TESTS = \
expr/expr_black \
expr/node_white \
expr/node_black \
expr/kind_black \
expr/node_builder_black \
expr/node_manager_white \
expr/attribute_white \
expr/attribute_black \
parser/parser_white \
context/context_black \
context/context_white \
context/context_mm_black \
context/cdo_black \
context/cdlist_black \
context/cdmap_black \
theory/theory_black \
theory/theory_uf_white \
util/assert_white \
util/configuration_white \
util/output_white \
util/integer_black \
util/integer_white \
util/rational_white
# 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)
if HAVE_CXXTESTGEN
AM_CPPFLAGS = \
-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
$(TEST_CPPFLAGS)
AM_CXXFLAGS = $(TEST_CXXFLAGS)
AM_LDFLAGS = $(TEST_LDFLAGS)
AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
AM_CXXFLAGS_PUBLIC =
AM_LDFLAGS_WHITE = \
@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
@abs_top_builddir@/src/libcvc4_noinst.la
AM_LDFLAGS_BLACK = \
@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
@abs_top_builddir@/src/libcvc4_noinst.la
AM_LDFLAGS_PUBLIC = \
@abs_top_builddir@/src/libcvc4.la
EXTRA_DIST = \
no_cxxtest \
$(TEST_DEPS_DIST)
MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
@mk_include@ @srcdir@/Makefile.tests
# We leave "TESTS" empty here; it's handled in Makefile.tests (see
# that file for comment)
# TESTS =
if STATIC_BINARY
unit_LINK = $(CXXLINK) -all-static
else
unit_LINK = $(CXXLINK)
endif
$(UNIT_TESTS:%=%.cpp): %.cpp: %.h
$(AM_V_at)mkdir -p `dirname "$@"`
$(AM_V_GEN)$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
$(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_WHITE) $@.lo
$(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS)
$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_BLACK) $@.lo
$(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_PUBLIC) $@.lo
else
# force a user-visible failure for "make check"
TESTS = no_cxxtest
EXTRA_DIST = \
$(UNIT_TESTS:%=%.cpp) \
$(TEST_DEPS_DIST)
endif
# trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
if CVC4_FALSE
noinst_LTLIBRARIES = libdummy.la
libdummy_la_SOURCES = expr/node_black.cpp
libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
endif
# synonyms for "check"
.PHONY: regress test
regress test: check
# in unit test dir, regressN are also synonyms for check
.PHONY: regress0 regress1 regress2 regress3
regress0 regress1 regress2 regress3: check
|