1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): acsys
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, and exceptions.
16 ** Assertion utility classes, functions, and exceptions. Implementation.
23 #include "util/Assert.h"
24 #include "util/exception.h"
32 CVC4_PUBLIC
CVC4_THREADLOCAL(const char*) s_debugLastException
= NULL
;
33 #endif /* CVC4_DEBUG */
35 void AssertionException::construct(const char* header
, const char* extra
,
36 const char* function
, const char* file
,
37 unsigned line
, const char* fmt
,
39 // try building the exception msg with a smallish buffer first,
40 // then with a larger one if sprintf tells us to.
49 size
= snprintf(buf
, n
, "%s\n%s\n%s:%d\n",
50 header
, function
, file
, line
);
52 size
= snprintf(buf
, n
, "%s\n%s\n%s:%d:\n\n %s\n",
53 header
, function
, file
, line
, extra
);
58 va_copy(args_copy
, args
);
59 size
+= vsnprintf(buf
+ size
, n
- size
, fmt
, args
);
68 // try again with a buffer that's large enough
74 setMessage(string(buf
));
77 if(s_debugLastException
== NULL
) {
78 // we leak buf[] but only in debug mode with assertions failing
79 s_debugLastException
= buf
;
81 #else /* CVC4_DEBUG */
83 #endif /* CVC4_DEBUG */
86 void AssertionException::construct(const char* header
, const char* extra
,
87 const char* function
, const char* file
,
89 // try building the exception msg with a smallish buffer first,
90 // then with a larger one if sprintf tells us to.
99 size
= snprintf(buf
, n
, "%s.\n%s\n%s:%d\n",
100 header
, function
, file
, line
);
102 size
= snprintf(buf
, n
, "%s.\n%s\n%s:%d:\n\n %s\n",
103 header
, function
, file
, line
, extra
);
109 // try again with a buffer that's large enough
115 setMessage(string(buf
));
118 // we leak buf[] but only in debug mode with assertions failing
119 if(s_debugLastException
== NULL
) {
120 s_debugLastException
= buf
;
122 #else /* CVC4_DEBUG */
124 #endif /* CVC4_DEBUG */
130 * Special assertion failure handling in debug mode; in non-debug
131 * builds, the exception is thrown from the macro. We factor out this
132 * additional logic so as not to bloat the code at every Assert()
135 * Note this name is prefixed with "debug" because it is included in
136 * debug builds only; in debug builds, it handles all assertion
137 * failures (even those that exist in non-debug builds).
139 void debugAssertionFailed(const AssertionException
& thisException
,
140 const char* propagatingException
) {
141 static CVC4_THREADLOCAL(bool) alreadyFired
= false;
143 if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired
) {
149 // propagatingException is the propagating exception, but can be
150 // NULL if the propagating exception is not a CVC4::Exception.
151 Warning() << "===========================================" << std::endl
152 << "An assertion failed during stack unwinding:" << std::endl
;
153 if(propagatingException
!= NULL
) {
154 Warning() << "The propagating exception is:" << std::endl
155 << propagatingException
<< std::endl
156 << "===========================================" << std::endl
;
157 Warning() << "The newly-thrown exception is:" << std::endl
;
159 Warning() << "The propagating exception is unknown." << std::endl
;
161 Warning() << thisException
<< std::endl
162 << "===========================================" << std::endl
;
167 #endif /* CVC4_DEBUG */
169 }/* CVC4 namespace */