summaryrefslogtreecommitdiff
path: root/test/unit/util
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/util')
-rw-r--r--test/unit/util/assert_white.h40
-rw-r--r--test/unit/util/configuration_black.h (renamed from test/unit/util/configuration_white.h)6
-rw-r--r--test/unit/util/exception_black.h58
-rw-r--r--test/unit/util/output_black.h304
-rw-r--r--test/unit/util/output_white.h97
5 files changed, 404 insertions, 101 deletions
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 9425daa44..d001c5a84 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -15,6 +15,9 @@
#include <cxxtest/TestSuite.h>
+#include <string>
+#include <cstring>
+
#include "util/Assert.h"
using namespace CVC4;
@@ -39,9 +42,44 @@ public:
TS_ASSERT_THROWS( Unimplemented(), UnimplementedOperationException );
TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException );
TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException );
- TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), IllegalArgumentException );
+ TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"),
+ IllegalArgumentException );
TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
}
+ void testReallyLongAssert() {
+ string msg(1034, 'x');
+ try {
+ AlwaysAssert(false, msg.c_str());
+ TS_FAIL("Should have thrown an exception !");
+ } catch(AssertionException& e) {
+ // we don't want to match on the entire string, because it may
+ // have an absolute path to the unit test binary, line number
+ // info, etc.
+ const char* theString = e.toString().c_str();
+ const char* firstPart =
+ "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n";
+ string lastPartStr = "\n\n false\n" + msg;
+ const char* lastPart = lastPartStr.c_str();
+ TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0);
+ TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart),
+ lastPart, strlen(lastPart)) == 0);
+ } catch(...) {
+ TS_FAIL("Threw the wrong kind of exception !");
+ }
+ }
+
+ void testUnreachable() {
+ TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException );
+ TS_ASSERT_THROWS( Unreachable("hello"), UnreachableCodeException );
+ TS_ASSERT_THROWS( Unreachable("hello %s", "world"), UnreachableCodeException );
+
+ int x = 5;
+ TS_ASSERT_THROWS( Unhandled(), UnhandledCaseException );
+ TS_ASSERT_THROWS( Unhandled(x), UnhandledCaseException );
+ TS_ASSERT_THROWS( Unhandled("foo"), UnhandledCaseException );
+ TS_ASSERT_THROWS( Unhandled("foo %s baz", "bar"), UnhandledCaseException );
+ }
+
};
diff --git a/test/unit/util/configuration_white.h b/test/unit/util/configuration_black.h
index 04cacc155..5ee4cf095 100644
--- a/test/unit/util/configuration_white.h
+++ b/test/unit/util/configuration_black.h
@@ -1,5 +1,5 @@
/********************* */
-/** configuration_white.h
+/** configuration_black.h
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
@@ -10,7 +10,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** White box testing of CVC4::Configuration.
+ ** Black box testing of CVC4::Configuration.
**/
#include <cxxtest/TestSuite.h>
@@ -20,7 +20,7 @@
using namespace CVC4;
using namespace std;
-class ConfigurationWhite : public CxxTest::TestSuite {
+class ConfigurationBlack : public CxxTest::TestSuite {
public:
diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
new file mode 100644
index 000000000..758a12645
--- /dev/null
+++ b/test/unit/util/exception_black.h
@@ -0,0 +1,58 @@
+/********************* */
+/** exception_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::Exception.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#include "util/exception.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ExceptionBlack : public CxxTest::TestSuite {
+public:
+
+ void setUp() {
+ }
+
+ void tearDown() {
+ }
+
+ // CVC4::Exception is a simple class, just test it all at once.
+ void testExceptions() {
+ Exception e1;
+ Exception e2(string("foo!"));
+ Exception e3("bar!");
+
+ TS_ASSERT_EQUALS(e1.toString(), string("Unknown exception"));
+ TS_ASSERT_EQUALS(e2.toString(), string("foo!"));
+ TS_ASSERT_EQUALS(e3.toString(), string("bar!"));
+
+ e1.setMessage("blah");
+ e2.setMessage("another");
+ e3.setMessage("three of 'em!");
+
+ stringstream s1, s2, s3;
+ s1 << e1;
+ s2 << e2;
+ s3 << e3;
+
+ TS_ASSERT_EQUALS(s1.str(), string("blah"));
+ TS_ASSERT_EQUALS(s2.str(), string("another"));
+ TS_ASSERT_EQUALS(s3.str(), string("three of 'em!"));
+ }
+};
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
new file mode 100644
index 000000000..6e613e9f4
--- /dev/null
+++ b/test/unit/util/output_black.h
@@ -0,0 +1,304 @@
+/********************* */
+/** output_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4 output classes.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#include "util/output.h"
+
+using namespace CVC4;
+using namespace std;
+
+class OutputBlack : public CxxTest::TestSuite {
+
+ stringstream d_debugStream;
+ stringstream d_traceStream;
+ stringstream d_noticeStream;
+ stringstream d_chatStream;
+ stringstream d_messageStream;
+ stringstream d_warningStream;
+
+public:
+
+ void setUp() {
+ Debug.setStream(d_debugStream);
+ Trace.setStream(d_traceStream);
+ Notice.setStream(d_noticeStream);
+ Chat.setStream(d_chatStream);
+ Message.setStream(d_messageStream);
+ Warning.setStream(d_warningStream);
+
+ d_debugStream.str("");
+ d_traceStream.str("");
+ d_noticeStream.str("");
+ d_chatStream.str("");
+ d_messageStream.str("");
+ d_warningStream.str("");
+ }
+
+ void tearDown() {
+ }
+
+ void testOutput() {
+ Debug.on("foo");
+ Debug("foo") << "testing1";
+ Debug.off("foo");
+ Debug("foo") << "testing2";
+ Debug.on("foo");
+ Debug("foo") << "testing3";
+
+ Message() << "a message";
+ Warning() << "bad warning!";
+ Chat() << "chatty";
+ Notice() << "note";
+
+ Trace.on("foo");
+ Trace("foo") << "tracing1";
+ Trace.off("foo");
+ Trace("foo") << "tracing2";
+ Trace.on("foo");
+ Trace("foo") << "tracing3";
+
+#ifdef CVC4_MUZZLE
+
+ TS_ASSERT( d_debugStream.str() == "" );
+ TS_ASSERT( d_messageStream.str() == "" );
+ TS_ASSERT( d_warningStream.str() == "" );
+ TS_ASSERT( d_chatStream.str() == "" );
+ TS_ASSERT( d_noticeStream.str() == "" );
+ TS_ASSERT( d_traceStream.str() == "" );
+
+#else /* CVC4_MUZZLE */
+
+# ifdef CVC4_DEBUG
+ TS_ASSERT( d_debugStream.str() == "testing1testing3" );
+# else /* CVC4_DEBUG */
+ TS_ASSERT( d_debugStream.str() == "" );
+# endif /* CVC4_DEBUG */
+
+ TS_ASSERT( d_messageStream.str() == "a message" );
+ TS_ASSERT( d_warningStream.str() == "bad warning!" );
+ TS_ASSERT( d_chatStream.str() == "chatty" );
+ TS_ASSERT( d_noticeStream.str() == "note" );
+
+# ifdef CVC4_TRACING
+ TS_ASSERT( d_traceStream.str() == "tracing1tracing3" );
+# else /* CVC4_TRACING */
+ TS_ASSERT( d_traceStream.str() == "" );
+# endif /* CVC4_TRACING */
+
+#endif /* CVC4_MUZZLE */
+ }
+
+ void testPrintf() {
+
+#ifdef CVC4_MUZZLE
+
+ Debug.off("yo");
+ Debug.printf("yo", "hello %s", "world");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+ Debug.printf(string("yo"), "hello %s", "world");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+
+ Debug.on("yo");
+ Debug.printf("yo", "hello %s", "world");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+ Debug.printf(string("yo"), "hello %s", "world");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+
+ Trace.off("yo");
+ Trace.printf("yo", "hello %s", "world");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+ Trace.printf(string("yo"), "hello %s", "world");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+
+ Trace.on("yo");
+ Trace.printf("yo", "hello %s", "world");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+ Trace.printf(string("yo"), "hello %s", "world");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+
+ Warning.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_warningStream.str(), string());
+
+ Chat.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_chatStream.str(), string());
+
+ Message.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_messageStream.str(), string());
+
+ Notice.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_noticeStream.str(), string());
+
+#else /* CVC4_MUZZLE */
+
+ Debug.off("yo");
+ Debug.printf("yo", "hello %s", "world");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+ Debug.printf(string("yo"), "hello %s", "world");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+
+ Debug.on("yo");
+ Debug.printf("yo", "hello %s", "world");
+#ifdef CVC4_DEBUG
+ TS_ASSERT_EQUALS(d_debugStream.str(), string("hello world"));
+#else /* CVC4_DEBUG */
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+#endif /* CVC4_DEBUG */
+ d_debugStream.str("");
+ Debug.printf(string("yo"), "hello %s", "world");
+#ifdef CVC4_DEBUG
+ TS_ASSERT_EQUALS(d_debugStream.str(), string("hello world"));
+#else /* CVC4_DEBUG */
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+#endif /* CVC4_DEBUG */
+ d_debugStream.str("");
+
+ Trace.off("yo");
+ Trace.printf("yo", "hello %s", "world");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+ Trace.printf(string("yo"), "hello %s", "world");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+
+ Trace.on("yo");
+ Trace.printf("yo", "hello %s", "world");
+#ifdef CVC4_TRACING
+ TS_ASSERT_EQUALS(d_traceStream.str(), string("hello world"));
+#else /* CVC4_TRACING */
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+#endif /* CVC4_TRACING */
+ d_traceStream.str("");
+ Trace.printf(string("yo"), "hello %s", "world");
+#ifdef CVC4_TRACING
+ TS_ASSERT_EQUALS(d_traceStream.str(), string("hello world"));
+#else /* CVC4_TRACING */
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+#endif /* CVC4_TRACING */
+
+ Warning.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_warningStream.str(), string("hello world"));
+
+ Chat.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_chatStream.str(), string("hello world"));
+
+ Message.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_messageStream.str(), string("hello world"));
+
+ Notice.printf("hello %s", "world");
+ TS_ASSERT_EQUALS(d_noticeStream.str(), string("hello world"));
+
+#endif /* CVC4_MUZZLE */
+
+ }
+
+ void testSimplePrint() {
+
+#ifdef CVC4_MUZZLE
+
+ Debug.off("yo");
+ Debug("yo", "foobar");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+ Debug.on("yo");
+ Debug("yo", "baz foo");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+
+ Trace.off("yo");
+ Trace("yo", "foobar");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+ Trace.on("yo");
+ Trace("yo", "baz foo");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+
+ Warning("baz foo");
+ TS_ASSERT_EQUALS(d_warningStream.str(), string());
+ d_warningStream.str("");
+
+ Chat("baz foo");
+ TS_ASSERT_EQUALS(d_chatStream.str(), string());
+ d_chatStream.str("");
+
+ Message("baz foo");
+ TS_ASSERT_EQUALS(d_messageStream.str(), string());
+ d_messageStream.str("");
+
+ Notice("baz foo");
+ TS_ASSERT_EQUALS(d_noticeStream.str(), string());
+ d_noticeStream.str("");
+
+#else /* CVC4_MUZZLE */
+
+ Debug.off("yo");
+ Debug("yo", "foobar");
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+ d_debugStream.str("");
+ Debug.on("yo");
+ Debug("yo", "baz foo");
+# ifdef CVC4_DEBUG
+ TS_ASSERT_EQUALS(d_debugStream.str(), string("baz foo"));
+# else /* CVC4_DEBUG */
+ TS_ASSERT_EQUALS(d_debugStream.str(), string());
+# endif /* CVC4_DEBUG */
+ d_debugStream.str("");
+
+ Trace.off("yo");
+ Trace("yo", "foobar");
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+ d_traceStream.str("");
+ Trace.on("yo");
+ Trace("yo", "baz foo");
+# ifdef CVC4_TRACING
+ TS_ASSERT_EQUALS(d_traceStream.str(), string("baz foo"));
+# else /* CVC4_TRACING */
+ TS_ASSERT_EQUALS(d_traceStream.str(), string());
+# endif /* CVC4_TRACING */
+ d_traceStream.str("");
+
+ Warning("baz foo");
+ TS_ASSERT_EQUALS(d_warningStream.str(), string("baz foo"));
+ d_warningStream.str("");
+
+ Chat("baz foo");
+ TS_ASSERT_EQUALS(d_chatStream.str(), string("baz foo"));
+ d_chatStream.str("");
+
+ Message("baz foo");
+ TS_ASSERT_EQUALS(d_messageStream.str(), string("baz foo"));
+ d_messageStream.str("");
+
+ Notice("baz foo");
+ TS_ASSERT_EQUALS(d_noticeStream.str(), string("baz foo"));
+ d_noticeStream.str("");
+
+#endif /* CVC4_MUZZLE */
+
+ }
+};
diff --git a/test/unit/util/output_white.h b/test/unit/util/output_white.h
deleted file mode 100644
index 7eda3db9d..000000000
--- a/test/unit/util/output_white.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/********************* */
-/** output_white.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** White box testing of CVC4::Configuration.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <sstream>
-
-#include "util/output.h"
-
-using namespace CVC4;
-using namespace std;
-
-class OutputWhite : public CxxTest::TestSuite {
-
- stringstream d_debugStream;
- stringstream d_traceStream;
- stringstream d_noticeStream;
- stringstream d_chatStream;
- stringstream d_messageStream;
- stringstream d_warningStream;
-
-public:
-
- void setUp() {
- Debug.setStream(d_debugStream);
- Trace.setStream(d_traceStream);
- Notice.setStream(d_noticeStream);
- Chat.setStream(d_chatStream);
- Message.setStream(d_messageStream);
- Warning.setStream(d_warningStream);
- }
-
- void testOutput() {
- Debug.on("foo");
- Debug("foo") << "testing1";
- Debug.off("foo");
- Debug("foo") << "testing2";
- Debug.on("foo");
- Debug("foo") << "testing3";
-
- Message() << "a message";
- Warning() << "bad warning!";
- Chat() << "chatty";
- Notice() << "note";
-
- Trace.on("foo");
- Trace("foo") << "tracing1";
- Trace.off("foo");
- Trace("foo") << "tracing2";
- Trace.on("foo");
- Trace("foo") << "tracing3";
-
-#ifdef CVC4_MUZZLE
-
- TS_ASSERT( d_debugStream.str() == "" );
- TS_ASSERT( d_messageStream.str() == "" );
- TS_ASSERT( d_warningStream.str() == "" );
- TS_ASSERT( d_chatStream.str() == "" );
- TS_ASSERT( d_noticeStream.str() == "" );
- TS_ASSERT( d_traceStream.str() == "" );
-
-#else /* CVC4_MUZZLE */
-
-# ifdef CVC4_DEBUG
- TS_ASSERT( d_debugStream.str() == "testing1testing3" );
-# else /* CVC4_DEBUG */
- TS_ASSERT( d_debugStream.str() == "" );
-# endif /* CVC4_DEBUG */
-
- TS_ASSERT( d_messageStream.str() == "a message" );
- TS_ASSERT( d_warningStream.str() == "bad warning!" );
- TS_ASSERT( d_chatStream.str() == "chatty" );
- TS_ASSERT( d_noticeStream.str() == "note" );
-
-# ifdef CVC4_TRACING
- TS_ASSERT( d_traceStream.str() == "tracing1tracing3" );
-# else /* CVC4_TRACING */
- TS_ASSERT( d_traceStream.str() == "" );
-# endif /* CVC4_TRACING */
-
-#endif /* CVC4_MUZZLE */
- }
-
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback