diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-24 21:03:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-24 21:03:35 +0000 |
commit | 811158832b74e3b101af2c7473f4e11a41377dd4 (patch) | |
tree | 07c55ab126dd7eb24239b615c987a490b182c8a6 /src/util | |
parent | f6968899de4d27c5bc986c3ac89972fbbe35c361 (diff) |
configure option adjustments as per 11/24 meeting; various fixes and improvements
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/assert.h | 76 | ||||
-rw-r--r-- | src/util/options.h | 8 | ||||
-rw-r--r-- | src/util/output.h | 135 |
3 files changed, 210 insertions, 9 deletions
diff --git a/src/util/assert.h b/src/util/assert.h index 24e3a4cdf..6691c1b04 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -7,20 +7,78 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Assertion utility classes, functions, and exceptions. **/ #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H -#include <cassert> +#include <string> +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" -#ifdef DEBUG -// the __builtin_expect() helps us if assert is built-in or a macro -# define cvc4assert(x) assert(__builtin_expect((x), 1)) -#else -// TODO: use a compiler annotation when assertions are off ? -// (to improve optimization) -# define cvc4assert(x) -#endif /* DEBUG */ +namespace CVC4 { + +class AssertionException : public Exception { +public: + AssertionException() : Exception() {} + AssertionException(std::string msg) : Exception(msg) {} + AssertionException(const char* msg) : Exception(msg) {} +};/* class AssertionException */ + +class UnreachableCodeException : public AssertionException { +public: + UnreachableCodeException() : AssertionException() {} + UnreachableCodeException(std::string msg) : AssertionException(msg) {} + UnreachableCodeException(const char* msg) : AssertionException(msg) {} +};/* class UnreachableCodeException */ + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg) + +#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) +#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg) + +inline void AssertImpl(const char* info, bool cond, std::string msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond, const char* msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(info); +} + +#ifdef __GNUC__ +inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnreachableImpl(const char* info, std::string msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info, const char* msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info) { + throw new UnreachableCodeException(info); +} + +}/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ diff --git a/src/util/options.h b/src/util/options.h index 490cd607b..54b4e2f9b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -10,6 +10,9 @@ ** [[ Add file-specific comments here ]] **/ +#include <iostream> + +#ifndef __CVC4__OPTIONS_H #define __CVC4__OPTIONS_H namespace CVC4 { @@ -20,6 +23,9 @@ struct Options { bool smtcomp_mode; bool statistics; + std::ostream *out; + std::ostream *err; + /* -1 means no output */ /* 0 is normal (and default) -- warnings only */ /* 1 is warnings + notices so the user doesn't get too bored */ @@ -32,6 +38,8 @@ struct Options { Options() : binary_name(), smtcomp_mode(false), statistics(false), + out(0), + err(0), verbosity(0), lang() {} diff --git a/src/util/output.h b/src/util/output.h new file mode 100644 index 000000000..4d3752849 --- /dev/null +++ b/src/util/output.h @@ -0,0 +1,135 @@ +/********************* -*- C++ -*- */ +/** output.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Output utility classes and functions. + **/ + +#ifndef __CVC4__OUTPUT_H +#define __CVC4__OUTPUT_H + +#include <iostream> +#include <string> +#include <set> +#include "util/exception.h" + +namespace CVC4 { + + +class Debug { + std::set<std::string> d_tags; + std::ostream &d_out; + +public: + static void operator()(const char* tag, const char*); + static void operator()(const char* tag, std::string); + static void operator()(string tag, const char*); + static void operator()(string tag, std::string); + + static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(const char* tag); + static std::ostream& operator()(std::string tag); + + static void on (const char* tag) { d_tags.insert(std::string(tag)); }; + static void on (std::string tag) { d_tags.insert(tag); }; + static void off(const char* tag) { d_tags.erase (std::string(tag)); }; + static void off(std::string tag) { d_tags.erase (tag); }; + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Debug */ + + +class Warning { + std::ostream &d_out; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Warning */ + + +class Notice { + std::ostream &d_os; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Notice */ + + +class Chat { + std::ostream &d_os; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Chat */ + + +class Trace { + std::ostream &d_os; + +public: + static void operator()(const char* tag, const char*); + static void operator()(const char* tag, std::string); + static void operator()(string tag, const char*); + static void operator()(string tag, std::string); + + static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + va_list vl; + va_start(vl, fmt); + vfprintf(buf, 1024, fmt, vl); + va_end(vl); + } + static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + + static std::ostream& operator()(const char* tag); + static std::ostream& operator()(std::string tag); + + static void on (const char* tag) { d_tags.insert(std::string(tag)); }; + static void on (std::string tag) { d_tags.insert(tag); }; + static void off(const char* tag) { d_tags.erase (std::string(tag)); }; + static void off(std::string tag) { d_tags.erase (tag); }; + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Trace */ + + +}/* CVC4 namespace */ + +#endif /* __CVC4__OUTPUT_H */ |