1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Assertion utility classes, functions, exceptions, and macros.
16 ** Assertion utility classes, functions, exceptions, and macros.
19 #include "cvc4_public.h"
21 #ifndef __CVC4__ASSERT_H
22 #define __CVC4__ASSERT_H
30 #include "util/exception.h"
31 #include "util/output.h"
36 class CVC4_PUBLIC AssertionException
: public Exception
{
38 void construct(const char* header
, const char* extra
,
39 const char* function
, const char* file
,
40 unsigned line
, const char* fmt
, ...) {
43 construct(header
, extra
, function
, file
, line
, fmt
, args
);
47 void construct(const char* header
, const char* extra
,
48 const char* function
, const char* file
,
49 unsigned line
, const char* fmt
, va_list args
);
51 void construct(const char* header
, const char* extra
,
52 const char* function
, const char* file
,
55 AssertionException() : Exception() {}
58 AssertionException(const char* extra
, const char* function
,
59 const char* file
, unsigned line
,
60 const char* fmt
, ...) :
64 construct("Assertion failure", extra
, function
, file
, line
, fmt
, args
);
68 AssertionException(const char* extra
, const char* function
,
69 const char* file
, unsigned line
) :
71 construct("Assertion failure", extra
, function
, file
, line
);
73 };/* class AssertionException */
75 class CVC4_PUBLIC UnreachableCodeException
: public AssertionException
{
77 UnreachableCodeException() : AssertionException() {}
80 UnreachableCodeException(const char* function
, const char* file
,
81 unsigned line
, const char* fmt
, ...) :
82 AssertionException() {
85 construct("Unreachable code reached",
86 NULL
, function
, file
, line
, fmt
, args
);
90 UnreachableCodeException(const char* function
, const char* file
,
92 AssertionException() {
93 construct("Unreachable code reached", NULL
, function
, file
, line
);
95 };/* class UnreachableCodeException */
97 class CVC4_PUBLIC UnhandledCaseException
: public UnreachableCodeException
{
99 UnhandledCaseException() : UnreachableCodeException() {}
102 UnhandledCaseException(const char* function
, const char* file
,
103 unsigned line
, const char* fmt
, ...) :
104 UnreachableCodeException() {
107 construct("Unhandled case encountered",
108 NULL
, function
, file
, line
, fmt
, args
);
113 UnhandledCaseException(const char* function
, const char* file
,
114 unsigned line
, T theCase
) :
115 UnreachableCodeException() {
116 std::stringstream sb
;
118 construct("Unhandled case encountered",
119 NULL
, function
, file
, line
, "The case was: %s", sb
.str().c_str());
122 UnhandledCaseException(const char* function
, const char* file
,
124 UnreachableCodeException() {
125 construct("Unhandled case encountered", NULL
, function
, file
, line
);
127 };/* class UnhandledCaseException */
129 class CVC4_PUBLIC UnimplementedOperationException
: public AssertionException
{
131 UnimplementedOperationException() : AssertionException() {}
134 UnimplementedOperationException(const char* function
, const char* file
,
135 unsigned line
, const char* fmt
, ...) :
136 AssertionException() {
139 construct("Unimplemented code encountered",
140 NULL
, function
, file
, line
, fmt
, args
);
144 UnimplementedOperationException(const char* function
, const char* file
,
146 AssertionException() {
147 construct("Unimplemented code encountered", NULL
, function
, file
, line
);
149 };/* class UnimplementedOperationException */
151 class CVC4_PUBLIC IllegalArgumentException
: public AssertionException
{
153 IllegalArgumentException() : AssertionException() {}
156 IllegalArgumentException(const char* argDesc
, const char* function
,
157 const char* file
, unsigned line
,
158 const char* fmt
, ...) :
159 AssertionException() {
162 construct("Illegal argument detected",
163 ( std::string(argDesc
) + " invalid" ).c_str(),
164 function
, file
, line
, fmt
, args
);
168 IllegalArgumentException(const char* argDesc
, const char* function
,
169 const char* file
, unsigned line
) :
170 AssertionException() {
171 construct("Illegal argument detected",
172 ( std::string(argDesc
) + " invalid" ).c_str(),
173 function
, file
, line
);
176 IllegalArgumentException(const char* condStr
, const char* argDesc
,
177 const char* function
, const char* file
,
178 unsigned line
, const char* fmt
, ...) :
179 AssertionException() {
182 construct("Illegal argument detected",
183 ( std::string(argDesc
) + " invalid; expected " +
184 condStr
+ " to hold" ).c_str(),
185 function
, file
, line
, fmt
, args
);
189 IllegalArgumentException(const char* condStr
, const char* argDesc
,
190 const char* function
, const char* file
,
192 AssertionException() {
193 construct("Illegal argument detected",
194 ( std::string(argDesc
) + " invalid; expected " +
195 condStr
+ " to hold" ).c_str(),
196 function
, file
, line
);
198 };/* class IllegalArgumentException */
203 extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException
;
204 #endif /* CVC4_DEBUG */
207 * Special assertion failure handling in debug mode; in non-debug
208 * builds, the exception is thrown from the macro. We factor out this
209 * additional logic so as not to bloat the code at every Assert()
212 * Note this name is prefixed with "debug" because it is included in
213 * debug builds only; in debug builds, it handles all assertion
214 * failures (even those that exist in non-debug builds).
216 void debugAssertionFailed(const AssertionException
& thisException
,
217 const char* lastException
) CVC4_PUBLIC
;
219 // If we're currently handling an exception, print a warning instead;
220 // otherwise std::terminate() is called by the runtime and we lose
221 // details of the exception
222 # define AlwaysAssert(cond, msg...) \
224 if(EXPECT_FALSE( ! (cond) )) { \
225 /* save the last assertion failure */ \
226 const char* lastException = s_debugLastException; \
227 AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
228 debugAssertionFailed(exception, lastException); \
232 #else /* CVC4_DEBUG */
233 // These simpler (but less useful) versions for non-debug builds fails
234 // will terminate() if thrown during stack unwinding.
235 # define AlwaysAssert(cond, msg...) \
237 if(EXPECT_FALSE( ! (cond) )) { \
238 throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
241 #endif /* CVC4_DEBUG */
243 #define Unreachable(msg...) \
244 throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
245 #define Unhandled(msg...) \
246 throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
247 #define Unimplemented(msg...) \
248 throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
249 #define IllegalArgument(arg, msg...) \
250 throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
251 #define CheckArgument(cond, arg, msg...) \
252 AlwaysAssertArgument(cond, arg, ## msg)
253 #define AlwaysAssertArgument(cond, arg, msg...) \
255 if(EXPECT_FALSE( ! (cond) )) { \
256 throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
260 #ifdef CVC4_ASSERTIONS
261 # define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
262 # define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
263 #else /* ! CVC4_ASSERTIONS */
264 # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
265 # define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
266 #endif /* CVC4_ASSERTIONS */
268 }/* CVC4 namespace */
270 #endif /* __CVC4__ASSERT_H */