From 65fa7fd4d674e00624657255c24748e580ef50d6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 22 Feb 2010 01:10:58 +0000 Subject: 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) --- test/unit/Makefile.am | 5 +- test/unit/expr/node_black.h | 4 ++ test/unit/util/assert_white.h | 47 +++++++++++++++++ test/unit/util/configuration_white.h | 95 +++++++++++++++++++++++++++++++++++ test/unit/util/output_white.h | 97 ++++++++++++++++++++++++++++++++++++ 5 files changed, 247 insertions(+), 1 deletion(-) create mode 100644 test/unit/util/assert_white.h create mode 100644 test/unit/util/configuration_white.h create mode 100644 test/unit/util/output_white.h (limited to 'test') diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 84465127b..c145cf752 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,7 +4,10 @@ UNIT_TESTS = \ expr/node_black \ parser/parser_black \ context/context_black \ - context/context_mm_black + context/context_mm_black \ + util/assert_white \ + util/configuration_white \ + util/output_white # Things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 0693b48db..102549c42 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -160,9 +160,11 @@ public: void testOperatorSquare() { /*Node operator[](int i) const */ +#ifdef CVC4_ASSERTIONS //Basic bounds check on a node w/out children TS_ASSERT_THROWS(Node::null()[-1], AssertionException); TS_ASSERT_THROWS(Node::null()[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ //Basic access check Node tb = d_nm->mkNode(TRUE); @@ -177,9 +179,11 @@ public: TS_ASSERT(tb == ite[1]); TS_ASSERT(eb == ite[2]); +#ifdef CVC4_ASSERTIONS //Bounds check on a node with children TS_ASSERT_THROWS(ite == ite[-1],AssertionException); TS_ASSERT_THROWS(ite == ite[4],AssertionException); +#endif /* CVC4_ASSERTIONS */ } /*tests: Node& operator=(const Node&); */ 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 + +#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") ); + } + +}; diff --git a/test/unit/util/configuration_white.h b/test/unit/util/configuration_white.h new file mode 100644 index 000000000..04cacc155 --- /dev/null +++ b/test/unit/util/configuration_white.h @@ -0,0 +1,95 @@ +/********************* */ +/** configuration_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 + +#include "util/configuration.h" + +using namespace CVC4; +using namespace std; + +class ConfigurationWhite : public CxxTest::TestSuite { + +public: + + void testStaticFlags() { + const bool debug = +#ifdef CVC4_DEBUG + true; +#else /* CVC4_DEBUG */ + false; +#endif /* CVC4_DEBUG */ + + const bool tracing = +#ifdef CVC4_TRACING + true; +#else /* CVC4_TRACING */ + false; +#endif /* CVC4_TRACING */ + + const bool muzzled = +#ifdef CVC4_MUZZLE + true; +#else /* CVC4_MUZZLE */ + false; +#endif /* CVC4_MUZZLE */ + + const bool assertions = +#ifdef CVC4_ASSERTIONS + true; +#else /* CVC4_ASSERTIONS */ + false; +#endif /* CVC4_ASSERTIONS */ + + const bool coverage = +#ifdef CVC4_COVERAGE + true; +#else /* CVC4_COVERAGE */ + false; +#endif /* CVC4_COVERAGE */ + + const bool profiling = +#ifdef CVC4_PROFILING + true; +#else /* CVC4_PROFILING */ + false; +#endif /* CVC4_PROFILING */ + + TS_ASSERT( Configuration::isDebugBuild() == debug ); + TS_ASSERT( Configuration::isTracingBuild() == tracing ); + TS_ASSERT( Configuration::isMuzzledBuild() == muzzled ); + TS_ASSERT( Configuration::isAssertionBuild() == assertions ); + TS_ASSERT( Configuration::isCoverageBuild() == coverage ); + TS_ASSERT( Configuration::isProfilingBuild() == profiling ); + } + + void testPackageName() { + TS_ASSERT( Configuration::getPackageName() == "cvc4" ); + } + + void testVersions() { + // just test that the functions exist + Configuration::getVersionString(); + Configuration::getVersionMajor(); + Configuration::getVersionMinor(); + Configuration::getVersionRelease(); + } + + void testAbout() { + // just test that the function exists + Configuration::about(); + } + +}; diff --git a/test/unit/util/output_white.h b/test/unit/util/output_white.h new file mode 100644 index 000000000..7eda3db9d --- /dev/null +++ b/test/unit/util/output_white.h @@ -0,0 +1,97 @@ +/********************* */ +/** 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 + +#include +#include + +#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 */ + } + +}; -- cgit v1.2.3