diff options
| -rw-r--r-- | config.h.in | 12 | ||||
| -rw-r--r-- | configure.ac | 16 | ||||
| -rw-r--r-- | src/expr/expr.cpp | 4 | ||||
| -rw-r--r-- | src/expr/node.cpp | 10 | ||||
| -rw-r--r-- | src/main/Makefile.am | 3 | ||||
| -rw-r--r-- | src/main/about.h | 34 | ||||
| -rw-r--r-- | src/main/getopt.cpp | 70 | ||||
| -rw-r--r-- | src/main/usage.h | 1 | ||||
| -rw-r--r-- | src/util/Makefile.am | 3 | ||||
| -rw-r--r-- | src/util/configuration.h | 116 | ||||
| -rw-r--r-- | src/util/output.cpp | 17 | ||||
| -rw-r--r-- | src/util/output.h | 92 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 5 | ||||
| -rw-r--r-- | test/unit/expr/node_black.h | 4 | ||||
| -rw-r--r-- | test/unit/util/assert_white.h | 47 | ||||
| -rw-r--r-- | test/unit/util/configuration_white.h | 95 | ||||
| -rw-r--r-- | test/unit/util/output_white.h | 97 |
17 files changed, 555 insertions, 71 deletions
diff --git a/config.h.in b/config.h.in index 788d688a9..798fd63fa 100644 --- a/config.h.in +++ b/config.h.in @@ -1,5 +1,17 @@ /* config.h.in. Generated from configure.ac by autoheader. */ +/* Major component of the version of CVC4. */ +#undef CVC4_MAJOR + +/* Minor component of the version of CVC4. */ +#undef CVC4_MINOR + +/* Release component of the version of CVC4. */ +#undef CVC4_RELEASE + +/* Full release string for CVC4. */ +#undef CVC4_RELEASE_STRING + /* Define to 1 if you have the <dlfcn.h> header file. */ #undef HAVE_DLFCN_H diff --git a/configure.ac b/configure.ac index 6ee45bbb9..c67da8ba2 100644 --- a/configure.ac +++ b/configure.ac @@ -10,7 +10,10 @@ AC_CONFIG_SRCDIR([src/include/cvc4_config.h]) AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) -CVC4_RELEASE=prerelease +CVC4_MAJOR=0 +CVC4_MINOR=0 +CVC4_RELEASE=0 +CVC4_RELEASE_STRING=prerelease # Libtool version numbers for libraries # Version numbers are in the form current:revision:age @@ -30,8 +33,8 @@ CVC4_RELEASE=prerelease # For guidance on when to change the version number, refer to the # developer's guide. -CVC4_LIBRARY_VERSION=0:0:0 -CVC4_PARSER_LIBRARY_VERSION=0:0:0 +CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE +CVC4_PARSER_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE # Using the AC_CANONICAL_* macros destroy the command line you get # from $@, which we want later for determining the build profile. So @@ -303,7 +306,7 @@ if test "$enable_profiling" = yes; then CVC4LDFLAGS="$CVC4LDFLAGS -pg" fi -AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE) +AM_INIT_AUTOMAKE(cvc4, $CVC4_RELEASE_STRING) AC_CONFIG_HEADERS([config.h]) # Initialize libtool's configuration options. @@ -408,6 +411,11 @@ AC_SUBST(BUILDING_STATIC) AC_SUBST(CVC4_LIBRARY_VERSION) AC_SUBST(CVC4_PARSER_LIBRARY_VERSION) +AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.]) +AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.]) +AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.]) +AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.]) + CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS" CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 0170296be..032735ff0 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -171,12 +171,14 @@ Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const { } void Expr::printAst(std::ostream & o, int indent) const{ - getNode().printAst(o,indent); + getNode().printAst(o, indent); } void Expr::debugPrint(){ +#ifndef CVC4_MUZZLE printAst(Warning()); Warning().flush(); +#endif /* ! CVC4_MUZZLE */ } diff --git a/src/expr/node.cpp b/src/expr/node.cpp index f3115b17e..644570b24 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -133,7 +133,7 @@ static void indent(ostream & o, int indent){ o << ' '; } -void Node::printAst(ostream & o, int ind) const{ +void Node::printAst(ostream & o, int ind) const { indent(o, ind); o << '('; o << getKind(); @@ -143,17 +143,19 @@ void Node::printAst(ostream & o, int ind) const{ }else if(getNumChildren() >= 1){ for(Node::iterator child = begin(); child != end(); ++child){ o << endl; - (*child).printAst(o, ind+1); + (*child).printAst(o, ind + 1); } o << endl; indent(o, ind); } o << ')'; } - -void Node::debugPrint(){ + +void Node::debugPrint() { +#ifndef CVC4_MUZZLE printAst(Warning(), 0); Warning().flush(); +#endif /* ! CVC4_MUZZLE */ } }/* CVC4 namespace */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 7c4f2d52d..04d717294 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -9,8 +9,7 @@ cvc4_SOURCES = \ getopt.cpp \ util.cpp \ main.h \ - usage.h \ - about.h + usage.h cvc4_LDADD = \ ../parser/libcvc4parser.la \ diff --git a/src/main/about.h b/src/main/about.h deleted file mode 100644 index 9dacdc8cc..000000000 --- a/src/main/about.h +++ /dev/null @@ -1,34 +0,0 @@ -/********************* */ -/** about.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. - ** - ** The "about" string for the CVC4 driver binary. - **/ - -#ifndef __CVC4__MAIN__ABOUT_H -#define __CVC4__MAIN__ABOUT_H - -namespace CVC4 { -namespace main { - -const char about[] = "\ -This is a pre-release of CVC4.\n\ -Copyright (C) 2009, 2010\n\ - The ACSys Group\n\ - Courant Institute of Mathematical Sciences,\n\ - New York University\n\ - New York, NY 10012 USA\n\ -"; - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__MAIN__ABOUT_H */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 8ace8e778..190f7bbf3 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -27,7 +27,7 @@ #include "main.h" #include "util/exception.h" #include "usage.h" -#include "about.h" +#include "util/configuration.h" #include "util/output.h" #include "util/options.h" #include "parser/parser.h" @@ -52,21 +52,47 @@ CNF conversions currently supported as arguments to the --cnf option:\n\ var variable-introduction method (new vars, no exp. blow up in # clauses)\n\ "; -// FIXME add a comment here describing the purpose of this +/** + * For the main getopt() routine, we need ways to switch on long + * options without clashing with short option characters. This is an + * enum of those long options. For long options (e.g. "--verbose") + * with a short option equivalent ("-v"), we use the single-letter + * short option; therefore, this enumeration starts at 256 to avoid + * any collision. + */ enum OptionValue { CNF = 256, /* no clash with char options */ SMTCOMP, STATS, SEGV_NOSPIN, PARSE_ONLY, - NO_CHECKING + NO_CHECKING, + SHOW_CONFIG };/* enum OptionValue */ -// FIXME add a comment here describing the option array +/** + * This is a table of long options. By policy, each short option + * should have an equivalent long option (but the reverse isn't the + * case), so this table should thus contain all command-line options. + * + * Each option in this array has four elements: + * + * 1. the long option string + * 2. argument behavior for the option: + * no_argument - no argument permitted + * required_argument - an argument is expected + * optional_argument - an argument is permitted but not required + * 3. this is a pointer to an int which is set to the 4th entry of the + * array if the option is present; or NULL, in which case + * getopt_long() returns the 4th entry + * 4. the return value for getopt_long() when this long option (or the + * value to set the 3rd entry to; see #3) + */ static struct option cmdlineOptions[] = { // name, has_arg, *flag, val { "help" , no_argument , NULL, 'h' }, { "version" , no_argument , NULL, 'V' }, + { "about" , no_argument , NULL, 'V' }, { "verbose" , no_argument , NULL, 'v' }, { "quiet" , no_argument , NULL, 'q' }, { "lang" , required_argument, NULL, 'L' }, @@ -76,7 +102,8 @@ static struct option cmdlineOptions[] = { { "stats" , no_argument , NULL, STATS }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, { "parse-only" , no_argument , NULL, PARSE_ONLY }, - { "no-checking", no_argument , NULL, NO_CHECKING } + { "no-checking", no_argument , NULL, NO_CHECKING }, + { "show-config", no_argument , NULL, SHOW_CONFIG } };/* if you add things to the above, please remember to update usage.h! */ /** Full argv[0] */ @@ -98,7 +125,17 @@ throw(OptionException) { } opts->binary_name = string(progName); - // FIXME add a comment here describing the option string + // The strange string in this call is the short option string. The + // initial '+' means that option processing stops as soon as a + // non-option argument is encountered. The initial ':' indicates + // that getopt_long() should return ':' instead of '?' for a missing + // option argument. Then, each letter is a valid short option for + // getopt_long(), and if it's encountered, getopt_long() returns + // that character. A ':' after an option character means an + // argument is required; two colons indicates an argument is + // optional; no colons indicate an argument is not permitted. + // cmdlineOptions specifies all the long-options and the return + // value for getopt_long() should they be encountered. while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) { @@ -109,7 +146,7 @@ throw(OptionException) { exit(1); case 'V': - fputs(about, stdout); + fputs(Configuration::about().c_str(), stdout); exit(0); case 'v': @@ -182,14 +219,27 @@ throw(OptionException) { opts->semanticChecks = false; break; + case SHOW_CONFIG: + fputs(Configuration::about().c_str(), stdout); + printf("\n"); + printf("version : %s\n", Configuration::getVersionString().c_str()); + printf("\n"); + printf("debug code: %s\n", Configuration::isDebugBuild() ? "yes" : "no"); + printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); + printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); + printf("assertions: %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); + printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); + printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); + exit(0); + case '?': - throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'"); + throw OptionException(string("can't understand option `") + argv[optind - 1] + "'"); case ':': - throw OptionException(string("option missing its required argument"));// + argv[optind - 1] + "' missing its required argument"); + throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); default: - throw OptionException(string("can't understand option"));//: `") + argv[optind - 1] + "'"); + throw OptionException(string("can't understand option:") + argv[optind - 1] + "'"); } } diff --git a/src/main/usage.h b/src/main/usage.h index 79b906d88..9a8175e2a 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -37,6 +37,7 @@ CVC4 options:\n\ --stats give statistics on exit\n\ --segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\ --parse-only exit after parsing input\n\ + --show-config show CVC4 static configuration\n\ "; }/* CVC4::main namespace */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 9bbf89fff..76414ebe1 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -19,4 +19,5 @@ libutil_la_SOURCES = \ output.cpp \ output.h \ result.h \ - unique_id.h + unique_id.h \ + configuration.h diff --git a/src/util/configuration.h b/src/util/configuration.h new file mode 100644 index 000000000..b761f1f22 --- /dev/null +++ b/src/util/configuration.h @@ -0,0 +1,116 @@ +/********************* */ +/** configuration.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): taking + ** 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. + ** + ** SmtEngine: the main public entry point of libcvc4. + **/ + +#ifndef __CVC4__CONFIGURATION_H +#define __CVC4__CONFIGURATION_H + +#include "config.h" +#include "cvc4_config.h" + +namespace CVC4 { + +/** + * Represents the (static) configuration of CVC4. + */ +class CVC4_PUBLIC Configuration { + + /** Private default ctor: Disallow construction of this class */ + Configuration(); + +public: + + static bool isDebugBuild() { +#ifdef CVC4_DEBUG + return true; +#else /* CVC4_DEBUG */ + return false; +#endif /* CVC4_DEBUG */ + } + + static bool isTracingBuild() { +#ifdef CVC4_TRACING + return true; +#else /* CVC4_TRACING */ + return false; +#endif /* CVC4_TRACING */ + } + + static bool isMuzzledBuild() { +#ifdef CVC4_MUZZLE + return true; +#else /* CVC4_MUZZLE */ + return false; +#endif /* CVC4_MUZZLE */ + } + + static bool isAssertionBuild() { +#ifdef CVC4_ASSERTIONS + return true; +#else /* CVC4_ASSERTIONS */ + return false; +#endif /* CVC4_ASSERTIONS */ + } + + static bool isCoverageBuild() { +#ifdef CVC4_COVERAGE + return true; +#else /* CVC4_COVERAGE */ + return false; +#endif /* CVC4_COVERAGE */ + } + + static bool isProfilingBuild() { +#ifdef CVC4_PROFILING + return true; +#else /* CVC4_PROFILING */ + return false; +#endif /* CVC4_PROFILING */ + } + + static std::string getPackageName() { + return PACKAGE; + } + + static std::string getVersionString() { + return VERSION; + } + + static unsigned getVersionMajor() { + return 0; + } + + static unsigned getVersionMinor() { + return 0; + } + + static unsigned getVersionRelease() { + return 0; + } + + static std::string about() { + return std::string("\ +This is a pre-release of CVC4.\n\ +Copyright (C) 2009, 2010\n\ + The ACSys Group\n\ + Courant Institute of Mathematical Sciences,\n\ + New York University\n\ + New York, NY 10012 USA\n"); + } + +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__CONFIGURATION_H */ diff --git a/src/util/output.cpp b/src/util/output.cpp index 278158ad1..e7ac3de90 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -27,12 +27,17 @@ namespace CVC4 { null_streambuf null_sb; ostream null_os(&null_sb); +NullDebugC debugNullCvc4Stream CVC4_PUBLIC; +NullC nullCvc4Stream CVC4_PUBLIC; + +#ifndef CVC4_MUZZLE + DebugC DebugOut(&cout); -WarningC Warning (&cerr); -MessageC Message (&cout); -NoticeC Notice (&cout); -ChatC Chat (&cout); -TraceC Trace (&cout); +WarningC WarningOut(&cerr); +MessageC MessageOut(&cout); +NoticeC NoticeOut(&cout); +ChatC ChatOut(&cout); +TraceC TraceOut(&cout); void DebugC::printf(const char* tag, const char* fmt, ...) { if(d_tags.find(string(tag)) != d_tags.end()) { @@ -122,4 +127,6 @@ void TraceC::printf(string tag, const char* fmt, ...) { } } +#endif /* CVC4_MUZZLE */ + }/* CVC4 namespace */ diff --git a/src/util/output.h b/src/util/output.h index 94841a1f5..ad42416d8 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -49,6 +49,8 @@ extern null_streambuf null_sb; /** A null output stream singleton */ extern std::ostream null_os CVC4_PUBLIC; +#ifndef CVC4_MUZZLE + /** The debug output class */ class CVC4_PUBLIC DebugC { std::set<std::string> d_tags; @@ -115,10 +117,10 @@ public: /** The debug output singleton */ extern DebugC DebugOut CVC4_PUBLIC; #ifdef CVC4_DEBUG - #define Debug DebugOut -#else - #define Debug if(0) DebugOut -#endif +# define Debug DebugOut +#else /* CVC4_DEBUG */ +# define Debug if(0) debugNullCvc4Stream +#endif /* CVC4_DEBUG */ /** The warning output class */ class CVC4_PUBLIC WarningC { @@ -138,7 +140,8 @@ public: };/* class Warning */ /** The warning output singleton */ -extern WarningC Warning CVC4_PUBLIC; +extern WarningC WarningOut CVC4_PUBLIC; +#define Warning WarningOut /** The message output class */ class CVC4_PUBLIC MessageC { @@ -158,7 +161,8 @@ public: };/* class Message */ /** The message output singleton */ -extern MessageC Message CVC4_PUBLIC; +extern MessageC MessageOut CVC4_PUBLIC; +#define Message MessageOut /** The notice output class */ class CVC4_PUBLIC NoticeC { @@ -178,7 +182,8 @@ public: };/* class Notice */ /** The notice output singleton */ -extern NoticeC Notice CVC4_PUBLIC; +extern NoticeC NoticeOut CVC4_PUBLIC; +#define Notice NoticeOut /** The chat output class */ class CVC4_PUBLIC ChatC { @@ -198,7 +203,8 @@ public: };/* class Chat */ /** The chat output singleton */ -extern ChatC Chat CVC4_PUBLIC; +extern ChatC ChatOut CVC4_PUBLIC; +#define Chat ChatOut /** The trace output class */ class CVC4_PUBLIC TraceC { @@ -241,7 +247,75 @@ public: };/* class Trace */ /** The trace output singleton */ -extern TraceC Trace CVC4_PUBLIC; +extern TraceC TraceOut CVC4_PUBLIC; +#ifdef CVC4_TRACING +# define Trace TraceOut +#else /* CVC4_TRACING */ +# define Trace if(0) debugNullCvc4Stream +#endif /* CVC4_TRACING */ + +#else /* ! CVC4_MUZZLE */ + +# define Debug if(0) debugNullCvc4Stream +# define Warning if(0) nullCvc4Stream +# define Message if(0) nullCvc4Stream +# define Notice if(0) nullCvc4Stream +# define Chat if(0) nullCvc4Stream +# define Trace if(0) debugNullCvc4Stream + +#endif /* ! CVC4_MUZZLE */ + +/** + * Same shape as DebugC/TraceC, but does nothing; designed for + * compilation of muzzled builds. None of these should ever be called + * in muzzled builds, but we offer this to the compiler so it doesn't complain. + */ +class CVC4_PUBLIC NullDebugC { +public: + NullDebugC() {} + NullDebugC(std::ostream* 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 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))) {} + + std::ostream& operator()(const char* tag) { return null_os; } + std::ostream& operator()(std::string tag) { return null_os; } + + void on (const char* tag) {} + void on (std::string tag) {} + void off(const char* tag) {} + void off(std::string tag) {} + + void setStream(std::ostream& os) {} +};/* class NullDebugC */ + +/** + * Same shape as WarningC/etc., but does nothing; designed for + * compilation of muzzled builds. None of these should ever be called + * in muzzled builds, but we offer this to the compiler so it doesn't + * complain. */ +class CVC4_PUBLIC NullC { +public: + NullC() {} + NullC(std::ostream* os) {} + + void operator()(const char*) {} + void operator()(std::string) {} + + void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {} + + std::ostream& operator()() { return null_os; } + + void setStream(std::ostream& os) {} +};/* class NullC */ + +extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC; +extern NullC nullCvc4Stream CVC4_PUBLIC; }/* CVC4 namespace */ 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 <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") ); + } + +}; 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 <cxxtest/TestSuite.h> + +#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 <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 */ + } + +}; |