testing framework, configure fixes, incorporations from meeting, continued work

4 files changed, 73 insertions, 0 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
new file mode 100644
index 000000000..bf74eaa47
--- /dev/null
+++ b/test/Makefile.am
@@ -0,0 +1,23 @@
+if HAVE_CXXTESTGEN
+
+AM_CPPFLAGS = -I. "-I$(CXXTEST)" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+AM_CXXFLAGS = -fno-access-control
+AM_LDFLAGS = -L@top_builddir@/src/libcvc4.a
+TESTS = \
+	expr/expr_black \
+	expr/expr_white
+
+%.cpp: %.h
+	$(CXXTESTGEN) --have-eh --have-std --error-printer -o $@ $<
+%: %.cpp
+	$(CXX) $(TEST_CPPFLAGS) $(AM_CPPFLAGS) $(TEST_CXXFLAGS) $(AM_CXXFLAGS) -o $@ $(TEST_LDFLAGS) $(AM_LDFLAGS) $< @top_builddir@/src/libcvc4.a
+
+MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
+
+else
+
+# force a user-visible failure for "make check"
+TESTS = no_cxxtest
+
+endif
+
diff --git a/test/expr/expr_black.h b/test/expr/expr_black.h
new file mode 100644
index 000000000..97746d1c4
--- /dev/null
+++ b/test/expr/expr_black.h
@@ -0,0 +1,19 @@
+/* Black box testing of CVC4::Expr. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "cvc4_expr.h"
+
+using namespace CVC4;
+
+class ExprBlack : public CxxTest::TestSuite {
+public:
+
+  void testNull() {
+    Expr::s_null;
+  }
+
+  void testCopyCtor() {
+    Expr e(Expr::s_null);
+  }
+};
diff --git a/test/expr/expr_white.h b/test/expr/expr_white.h
new file mode 100644
index 000000000..b6bfdd394
--- /dev/null
+++ b/test/expr/expr_white.h
@@ -0,0 +1,19 @@
+/* White box testing of CVC4::Expr. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "cvc4_expr.h"
+
+using namespace CVC4;
+
+class ExprWhite : public CxxTest::TestSuite {
+public:
+
+  void testNull() {
+    Expr::s_null;
+  }
+
+  void testCopyCtor() {
+    Expr e(Expr::s_null);
+  }
+};
diff --git a/test/no_cxxtest b/test/no_cxxtest
new file mode 100755
index 000000000..cf8b8d729
--- /dev/null
+++ b/test/no_cxxtest
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+echo
+echo '***************************************************************************'
+echo '*                                                                         *'
+echo '*  ERROR:  CxxTest was not found at configure-time; tests cannot be run.  *'
+echo '*                                                                         *'
+echo '***************************************************************************'
+echo
+
+exit 1
+