diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-17 18:48:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-17 18:48:39 +0000 |
commit | 7eb18a6c4b0ec6fcf4b6474d22307baa04f8f515 (patch) | |
tree | 8621e2e60756ec6770bc949877eef808e7e99d55 /src/util | |
parent | 3b06265b82d48074b3b733d655efd6dab6481150 (diff) |
+ test infrastructure fixes
+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.h | 39 | ||||
-rw-r--r-- | src/util/output.cpp | 1 | ||||
-rw-r--r-- | src/util/output.h | 18 |
3 files changed, 56 insertions, 2 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h index c3b81727c..26a1ee7d4 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -122,7 +122,8 @@ public: va_list args; va_start(args, fmt); construct("Illegal argument detected", - argDesc, function, file, line, fmt, args); + ( std::string(argDesc) + " invalid" ).c_str(), + function, file, line, fmt, args); va_end(args); } @@ -130,7 +131,31 @@ public: const char* file, unsigned line) : AssertionException() { construct("Illegal argument detected", - argDesc, function, file, line); + ( std::string(argDesc) + " invalid" ).c_str(), + function, file, line); + } + + IllegalArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string(argDesc) + " invalid; expected " + + condStr + " to hold" ).c_str(), + function, file, line, fmt, args); + va_end(args); + } + + IllegalArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Illegal argument detected", + ( std::string(argDesc) + " invalid; expected " + + condStr + " to hold" ).c_str(), + function, file, line); } };/* class IllegalArgumentException */ @@ -146,11 +171,21 @@ public: throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define CheckArgument(cond, arg, msg...) \ + AlwaysAssertArgument(cond, arg, ## msg) +#define AlwaysAssertArgument(cond, arg, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) AlwaysAssert(cond, ## msg) +# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ }/* CVC4 namespace */ diff --git a/src/util/output.cpp b/src/util/output.cpp index e07f32a66..103a3d61a 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -22,6 +22,7 @@ std::ostream null_os(&null_sb); DebugC Debug (&std::cout); WarningC Warning(&std::cerr); +MessageC Message(&std::cout); NoticeC Notice (&std::cout); ChatC Chat (&std::cout); TraceC Trace (&std::cout); diff --git a/src/util/output.h b/src/util/output.h index b6532b93a..43dfe8a40 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -91,6 +91,24 @@ public: extern WarningC Warning CVC4_PUBLIC; +class CVC4_PUBLIC MessageC { + std::ostream *d_os; + +public: + MessageC(std::ostream* os) : d_os(os) {} + + 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))); + + std::ostream& operator()() { return *d_os; } + + void setStream(std::ostream& os) { d_os = &os; } +};/* class Message */ + +extern MessageC Message CVC4_PUBLIC; + class CVC4_PUBLIC NoticeC { std::ostream *d_os; |