diff options
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/assert_white.h | 40 | ||||
-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.h | 58 | ||||
-rw-r--r-- | test/unit/util/output_black.h | 304 | ||||
-rw-r--r-- | test/unit/util/output_white.h | 97 |
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 */ - } - -}; |