/* 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
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
# 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
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.
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"
}
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 */
}
o << ' ';
}
-void Node::printAst(ostream & o, int ind) const{
+void Node::printAst(ostream & o, int ind) const {
indent(o, ind);
o << '(';
o << getKind();
}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 */
getopt.cpp \
util.cpp \
main.h \
- usage.h \
- about.h
+ usage.h
cvc4_LDADD = \
../parser/libcvc4parser.la \
+++ /dev/null
-/********************* */
-/** 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 */
#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"
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' },
{ "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] */
}
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) {
exit(1);
case 'V':
- fputs(about, stdout);
+ fputs(Configuration::about().c_str(), stdout);
exit(0);
case 'v':
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] + "'");
}
}
--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 */
output.cpp \
output.h \
result.h \
- unique_id.h
+ unique_id.h \
+ configuration.h
--- /dev/null
+/********************* */
+/** 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 */
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()) {
}
}
+#endif /* CVC4_MUZZLE */
+
}/* CVC4 namespace */
/** 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;
/** 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 {
};/* 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 {
};/* 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 {
};/* 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 {
};/* 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 {
};/* 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 */
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
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);
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&); */
--- /dev/null
+/********************* */
+/** 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") );
+ }
+
+};
--- /dev/null
+/********************* */
+/** 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();
+ }
+
+};
--- /dev/null
+/********************* */
+/** 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 */
+ }
+
+};
projects / cvc5.git / commitdiff