From e390a4207d3858927354b3d4b40d540c00f8064c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 9 Apr 2010 16:25:32 +0000 Subject: [PATCH] added experimental "make lcov" target (it runs only unit tests); better coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes --- Makefile.am | 45 +++ src/context/cdlist.h | 1 + src/context/cdmap.h | 24 +- src/expr/metakind_template.h | 1 - src/util/output.h | 35 +- test/unit/Makefile.am | 8 +- test/unit/Makefile.tests | 2 +- test/unit/context/cdlist_black.h | 62 +++- test/unit/context/cdmap_white.h | 52 +++ test/unit/context/context_black.h | 51 +++ .../unit/expr/{expr_black.h => expr_public.h} | 6 +- test/unit/theory/theory_black.h | 2 +- test/unit/theory/theory_uf_white.h | 15 +- test/unit/util/assert_white.h | 40 ++- ...guration_white.h => configuration_black.h} | 6 +- test/unit/util/exception_black.h | 58 ++++ test/unit/util/output_black.h | 304 ++++++++++++++++++ test/unit/util/output_white.h | 97 ------ 18 files changed, 659 insertions(+), 150 deletions(-) create mode 100644 test/unit/context/cdmap_white.h rename test/unit/expr/{expr_black.h => expr_public.h} (99%) rename test/unit/util/{configuration_white.h => configuration_black.h} (94%) create mode 100644 test/unit/util/exception_black.h create mode 100644 test/unit/util/output_black.h delete mode 100644 test/unit/util/output_white.h diff --git a/Makefile.am b/Makefile.am index 5aec4e904..c10bc1263 100644 --- a/Makefile.am +++ b/Makefile.am @@ -11,3 +11,48 @@ SUBDIRS = src test contrib regress0 regress1 regress2 regress3: all (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 +LCOV = lcov +GENHTML = genhtml + +LCOV_EXCLUDES = \ + "$(CXXTEST)/*" \ + "/usr/include/*" \ + "$(abs_top_builddir)/test/*" + +# lcov 1.7 has some bugs that we have to work around (can't do +# baseline measurement, merge between different test-names doesn't +# work...) +.PHONY: lcov +lcov: all + $(LCOV) -z -d . + $(MAKE) check -C test/unit + $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info + $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES) + mkdir -p "@top_srcdir@/html" + $(GENHTML) -o "@top_srcdir@/html" cvc4-coverage.info + @echo "De-mangling C++ symbols..." + @find "@top_srcdir@/html" -name '*.func.html' | \ + xargs perl -pi -e 's#()(.*)()#$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3\n";#e' + +# when we get a working lcov, we can do better stats for +# modules/test-types; unfortunately lcov 1.8 directory paths +# are broken(?) or at least different than 1.7 +.PHONY: lcov18 +lcov18: all + @for testtype in public black white; do \ + echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \ + echo $(LCOV) -z -d .; \ + $(LCOV) -z -d . || exit 1; \ + echo $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \ + $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \ + echo $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \ + $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \ + echo $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES); \ + $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES) || exit 1; \ + echo; \ + done + mkdir -p "@top_srcdir@/html" + $(GENHTML) -o "@top_srcdir@/html" cvc4-coverage-public.info cvc4-coverage-black.info cvc4-coverage-white.info + @echo "De-mangling C++ symbols..." + @find "@top_srcdir@/html" -name '*.func.html' | \ + xargs perl -pi -e 's,()(.*)(),$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3";,e' diff --git a/src/context/cdlist.h b/src/context/cdlist.h index b0161c562..a2abc08d8 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -95,6 +95,7 @@ private: CDList(const CDList& l) : ContextObj(l), d_list(NULL), + d_callDestructor(l.d_callDestructor), d_size(l.d_size), d_sizeAlloc(0) { } diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 75f6eb2ae..4621d7fc5 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -140,24 +140,6 @@ public: } };/* class CDOmap<> */ -// Dummy subclass of ContextObj to serve as our data class -class CDMapData : public ContextObj { - // befriend CDMap<> so that it can allocate us - template - friend class CDMap; - - ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDMapData(*this); - } - - void restore(ContextObj* data) {} - -public: - - CDMapData(Context* context) : ContextObj(context) {} - CDMapData(const ContextObj& co) : ContextObj(co) {} - ~CDMapData() throw(AssertionException) { destroy(); } -}; /** * Generic templated class for a map which must be saved and restored @@ -181,11 +163,13 @@ class CDMap : public ContextObj { // Nothing to save; the elements take care of themselves virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDMapData(*this); + Unreachable(); } // Similarly, nothing to restore - virtual void restore(ContextObj* data) {} + virtual void restore(ContextObj* data) { + Unreachable(); + } void emptyTrash() { //FIXME multithreading diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 96152d075..fda2801be 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -199,7 +199,6 @@ inline bool NodeValueConstCompare::compare(const ::CVC4::expr::NodeValu if(x->d_nchildren == 1) { Assert(y->d_nchildren == 0); return compare(y, x); - return *reinterpret_cast(x->d_children[0]) == y->getConst(); } else if(y->d_nchildren == 1) { Assert(x->d_nchildren == 0); return x->getConst() == *reinterpret_cast(y->d_children[0]); diff --git a/src/util/output.h b/src/util/output.h index 6315389e8..79bdd788e 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -172,8 +172,8 @@ class CVC4_PUBLIC NoticeC { public: NoticeC(std::ostream* os) : d_os(os) {} - void operator()(const char*); - void operator()(std::string); + void operator()(const char* s) { *d_os << s; } + void operator()(std::string s) { *d_os << s; } void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); @@ -193,8 +193,8 @@ class CVC4_PUBLIC ChatC { public: ChatC(std::ostream* os) : d_os(os) {} - void operator()(const char*); - void operator()(std::string); + void operator()(const char* s) { *d_os << s; } + void operator()(std::string s) { *d_os << s; } void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); @@ -215,10 +215,29 @@ class CVC4_PUBLIC TraceC { public: TraceC(std::ostream* os) : d_os(os) {} - void operator()(const char* tag, const char*); - void operator()(const char* tag, std::string); - void operator()(std::string tag, const char*); - void operator()(std::string tag, std::string); + void operator()(const char* tag, const char* s) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const char* tag, const std::string& s) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const std::string& tag, const char* s) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const std::string& tag, const std::string& s) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + *d_os << s; + } + } void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index c52ac5d1c..3f0816560 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,6 +1,6 @@ # All unit tests UNIT_TESTS = \ - expr/expr_black \ + expr/expr_public \ expr/node_white \ expr/node_black \ expr/kind_black \ @@ -16,11 +16,13 @@ UNIT_TESTS = \ context/cdo_black \ context/cdlist_black \ context/cdmap_black \ + context/cdmap_white \ theory/theory_black \ theory/theory_uf_white \ util/assert_white \ - util/configuration_white \ - util/output_white \ + util/configuration_black \ + util/output_black \ + util/exception_black \ util/integer_black \ util/integer_white \ util/rational_white diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests index 4f2f3dd5f..e3ec536ce 100644 --- a/test/unit/Makefile.tests +++ b/test/unit/Makefile.tests @@ -8,7 +8,7 @@ # It's a pain to make automake happy. # Add "filtered" tests to the set of TESTS -TESTS = $(filter $(TEST_PREFIX)%,$(UNIT_TESTS)) +TESTS = $(filter $(TEST_PREFIX)%,$(filter %$(TEST_SUFFIX),$(UNIT_TESTS))) # subsets of the tests, based on name WHITE_TESTS = $(filter %_white,$(UNIT_TESTS)) diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index f31d5f273..418357630 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -23,6 +23,14 @@ using namespace std; using namespace CVC4::context; + +struct DtorSensitiveObject { + bool& d_dtorCalled; + DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {} + ~DtorSensitiveObject() { d_dtorCalled = true; } +}; + + class CDListBlack : public CxxTest::TestSuite { private: @@ -34,6 +42,10 @@ public: d_context = new Context(); } + void tearDown() { + delete d_context; + } + // test at different sizes. this triggers grow() behavior differently. // grow() was completely broken in revision 256 void testCDList10() { listTest(10); } @@ -44,7 +56,12 @@ public: void testCDList99() { listTest(99); } void listTest(int N) { - CDList list(d_context); + listTest(N, true); + listTest(N, false); + } + + void listTest(int N, bool callDestructor) { + CDList list(d_context, callDestructor); TS_ASSERT(list.empty()); for(int i = 0; i < N; ++i) { @@ -66,7 +83,46 @@ public: } } - void tearDown() { - delete d_context; + void testDtorCalled() { + bool shouldRemainFalse = false; + bool shouldFlipToTrue = false; + bool alsoFlipToTrue = false; + bool shouldAlsoRemainFalse = false; + bool aThirdFalse = false; + + CDList listT(d_context, true); + CDList listF(d_context, false); + + DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse); + DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue); + DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue); + DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse); + DtorSensitiveObject aThirdFalseDSO(aThirdFalse); + + listT.push_back(shouldAlsoRemainFalseDSO); + listF.push_back(shouldAlsoRemainFalseDSO); + + d_context->push(); + + listT.push_back(shouldFlipToTrueDSO); + listT.push_back(alsoFlipToTrueDSO); + + listF.push_back(shouldRemainFalseDSO); + listF.push_back(shouldAlsoRemainFalseDSO); + listF.push_back(aThirdFalseDSO); + + TS_ASSERT_EQUALS(shouldRemainFalse, false); + TS_ASSERT_EQUALS(shouldFlipToTrue, false); + TS_ASSERT_EQUALS(alsoFlipToTrue, false); + TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); + TS_ASSERT_EQUALS(aThirdFalse, false); + + d_context->pop(); + + TS_ASSERT_EQUALS(shouldRemainFalse, false); + TS_ASSERT_EQUALS(shouldFlipToTrue, true); + TS_ASSERT_EQUALS(alsoFlipToTrue, true); + TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); + TS_ASSERT_EQUALS(aThirdFalse, false); } }; diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h new file mode 100644 index 000000000..9a920ede8 --- /dev/null +++ b/test/unit/context/cdmap_white.h @@ -0,0 +1,52 @@ +/********************* */ +/** cdmap_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::context::CDMap<>. + **/ + +#include + +#include "context/cdmap.h" +#include "util/Assert.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class CDMapWhite : public CxxTest::TestSuite { + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + } + + void tearDown() { + delete d_context; + } + + void testUnreachableSaveAndRestore() { + CDMap map(d_context); + + TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); + + TS_ASSERT_THROWS(map.update(), UnreachableCodeException); + + TS_ASSERT_THROWS(map.save(d_context->getCMM()), UnreachableCodeException); + TS_ASSERT_THROWS(map.restore(&map), UnreachableCodeException); + + d_context->push(); + TS_ASSERT_THROWS(map.makeCurrent(), UnreachableCodeException); + } +}; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 549d99369..37c94aaad 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -60,4 +60,55 @@ public: d_context->push(); i = 5; } + + void testPreNotify() { + struct MyContextNotifyObj : ContextNotifyObj { + int nCalls; + + MyContextNotifyObj(Context* context, bool pre) : + ContextNotifyObj(context, pre), + nCalls(0) { + } + + void notify() { + ++nCalls; + } + } a(d_context, true), b(d_context, false); + + { + MyContextNotifyObj c(d_context, true), d(d_context, false); + + TS_ASSERT_EQUALS(a.nCalls, 0); + TS_ASSERT_EQUALS(b.nCalls, 0); + TS_ASSERT_EQUALS(c.nCalls, 0); + TS_ASSERT_EQUALS(d.nCalls, 0); + + d_context->push(); + d_context->push(); + + TS_ASSERT_EQUALS(a.nCalls, 0); + TS_ASSERT_EQUALS(b.nCalls, 0); + TS_ASSERT_EQUALS(c.nCalls, 0); + TS_ASSERT_EQUALS(d.nCalls, 0); + + d_context->pop(); + + TS_ASSERT_EQUALS(a.nCalls, 1); + TS_ASSERT_EQUALS(b.nCalls, 1); + TS_ASSERT_EQUALS(c.nCalls, 1); + TS_ASSERT_EQUALS(d.nCalls, 1); + + d_context->pop(); + + TS_ASSERT_EQUALS(a.nCalls, 2); + TS_ASSERT_EQUALS(b.nCalls, 2); + TS_ASSERT_EQUALS(c.nCalls, 2); + TS_ASSERT_EQUALS(d.nCalls, 2); + } + + // we do this to get full code coverage of destruction paths + delete d_context; + + d_context = NULL; + } }; diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_public.h similarity index 99% rename from test/unit/expr/expr_black.h rename to test/unit/expr/expr_public.h index 936381cd6..fd36a7cfa 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_public.h @@ -1,5 +1,5 @@ /********************* */ -/** expr_black.h +/** expr_public.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. ** - ** Black box testing of CVC4::Expr. + ** Public black-box testing of CVC4::Expr. **/ #include @@ -27,7 +27,7 @@ using namespace CVC4; using namespace CVC4::kind; using namespace std; -class ExprBlack : public CxxTest::TestSuite { +class ExprPublic : public CxxTest::TestSuite { private: ExprManager* d_em; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 24c8e407c..097724d48 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -243,7 +243,7 @@ public: TS_ASSERT_EQUALS(got, x_eq_f_f_x); - TS_ASSERT_EQUALS(7, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index c02214a25..f5da06a0b 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -154,13 +154,13 @@ public: d_euf->check(d_level); //Test that no additional calls to the output channel occurred. - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); d_euf->assertFact( f5_x_eq_x ); d_euf->check(d_level); - TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(2u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(1)); Node firstConflict = d_outputChannel.getIthNode(0); @@ -189,7 +189,7 @@ public: d_euf->assertFact(f_f_f_x_neq_f_x); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); @@ -205,7 +205,7 @@ public: d_euf->assertFact(x_neq_x); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0)); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); } @@ -218,7 +218,7 @@ public: d_euf->assertFact(x_eq_x); d_euf->check(d_level); - TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls()); } @@ -251,7 +251,7 @@ public: d_euf->assertFact( f1_x_neq_x ); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); TS_ASSERT_EQUALS(expectedConflict, realConflict); @@ -282,7 +282,4 @@ public: d_euf->check(d_level); } - - - }; 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 +#include +#include + #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 similarity index 94% rename from test/unit/util/configuration_white.h rename to 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 @@ -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 + +#include +#include + +#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 + +#include +#include + +#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 - -#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 */ - } - -}; -- 2.30.2