diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-22 01:10:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-22 01:10:58 +0000 |
commit | 65fa7fd4d674e00624657255c24748e580ef50d6 (patch) | |
tree | 1a5591fca4c3a9ab24d576c282f36607cb81a7f5 /test/unit/util/assert_white.h | |
parent | 7697b5218118d71800318472a7423a5b42bee469 (diff) |
fix bug 22 (remove tracing from non-trace builds; remove all output
from muzzled builds)
add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)
add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class
main driver now gets about() information from CVC4::Configuration.
configure.ac now more flexible at specifying major/minor/release
versions of CVC4
add --show-config option that dumps CVC4's static configuration
commented option processing strings in src/main/getopt.cpp
fixed some compilation problems for muzzled builds.
fixed some test code for non-assertion builds (where no assertions are expected)
Diffstat (limited to 'test/unit/util/assert_white.h')
-rw-r--r-- | test/unit/util/assert_white.h | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h new file mode 100644 index 000000000..9425daa44 --- /dev/null +++ b/test/unit/util/assert_white.h @@ -0,0 +1,47 @@ +/********************* */ +/** assert_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 "util/Assert.h" + +using namespace CVC4; +using namespace std; + +class AssertWhite : public CxxTest::TestSuite { +public: + + void testAssert() { +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( Assert(false), AssertionException ); + TS_ASSERT_THROWS( AssertArgument(false, "x"), IllegalArgumentException ); +#else /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS_NOTHING( Assert(false) ); + TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") ); +#endif /* CVC4_ASSERTIONS */ + + TS_ASSERT_THROWS_NOTHING( Assert(true) ); + TS_ASSERT_THROWS( AlwaysAssert(false), AssertionException ); + TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException ); + TS_ASSERT_THROWS( Unhandled(), UnhandledCaseException ); + 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_NOTHING( AssertArgument(true, "x") ); + TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); + } + +}; |