summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/cvc4_assert.cpp26
-rw-r--r--src/base/cvc4_assert.h9
-rw-r--r--src/base/exception.cpp49
-rw-r--r--src/base/exception.h26
-rw-r--r--src/expr/node.cpp7
-rw-r--r--src/main/util.cpp18
6 files changed, 102 insertions, 33 deletions
diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
index 6e51845dd..efc71c986 100644
--- a/src/base/cvc4_assert.cpp
+++ b/src/base/cvc4_assert.cpp
@@ -26,9 +26,10 @@ using namespace std;
namespace CVC4 {
#ifdef CVC4_DEBUG
-CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
+//CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
#endif /* CVC4_DEBUG */
+
void AssertionException::construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt,
@@ -71,13 +72,14 @@ void AssertionException::construct(const char* header, const char* extra,
setMessage(string(buf));
#ifdef CVC4_DEBUG
- if(s_debugLastException == NULL) {
- // we leak buf[] but only in debug mode with assertions failing
- s_debugLastException = buf;
+ LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
+ if(buffer != NULL){
+ if(buffer->getContents() == NULL) {
+ buffer->setContents(buf);
+ }
}
-#else /* CVC4_DEBUG */
- delete [] buf;
#endif /* CVC4_DEBUG */
+ delete [] buf;
}
void AssertionException::construct(const char* header, const char* extra,
@@ -111,14 +113,16 @@ void AssertionException::construct(const char* header, const char* extra,
setMessage(string(buf));
+
#ifdef CVC4_DEBUG
- // we leak buf[] but only in debug mode with assertions failing
- if(s_debugLastException == NULL) {
- s_debugLastException = buf;
+ LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
+ if(buffer != NULL){
+ if(buffer->getContents() == NULL) {
+ buffer->setContents(buf);
+ }
}
-#else /* CVC4_DEBUG */
- delete [] buf;
#endif /* CVC4_DEBUG */
+ delete [] buf;
}
#ifdef CVC4_DEBUG
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
index 6b47de8cc..63ed6d53e 100644
--- a/src/base/cvc4_assert.h
+++ b/src/base/cvc4_assert.h
@@ -235,8 +235,6 @@ public:
#ifdef CVC4_DEBUG
-extern CVC4_THREADLOCAL(const char*) s_debugLastException;
-
/**
* Special assertion failure handling in debug mode; in non-debug
* builds, the exception is thrown from the macro. We factor out this
@@ -254,9 +252,12 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
// details of the exception
# define AlwaysAssert(cond, msg...) \
do { \
- if(__builtin_expect( ( ! (cond) ), false )) { \
+ if(__builtin_expect( ( ! (cond) ), false )) { \
/* save the last assertion failure */ \
- const char* lastException = ::CVC4::s_debugLastException; \
+ ::CVC4::LastExceptionBuffer* buffer = \
+ ::CVC4::LastExceptionBuffer::getCurrent(); \
+ const char* lastException = (buffer == NULL) ? \
+ NULL : buffer->getContents(); \
::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
::CVC4::debugAssertionFailed(exception, lastException); \
} \
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index 87bdfcfa5..e1486e5bc 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -16,10 +16,11 @@
#include "base/exception.h"
-#include <string>
+#include <cstdarg>
#include <cstdio>
#include <cstdlib>
-#include <cstdarg>
+#include <cstring>
+#include <string>
#include "base/cvc4_assert.h"
@@ -27,6 +28,28 @@ using namespace std;
namespace CVC4 {
+CVC4_THREADLOCAL(LastExceptionBuffer*) LastExceptionBuffer::s_currentBuffer = NULL;
+
+LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {}
+
+LastExceptionBuffer::~LastExceptionBuffer() {
+ if(d_contents != NULL){
+ free(d_contents);
+ d_contents = NULL;
+ }
+}
+
+void LastExceptionBuffer::setContents(const char* string) {
+ if(d_contents != NULL){
+ free(d_contents);
+ d_contents = NULL;
+ }
+
+ if(string != NULL){
+ d_contents = strdup(string);
+ }
+}
+
char* IllegalArgumentException::s_header = "Illegal argument detected";
std::string IllegalArgumentException::formatVariadic() {
@@ -107,13 +130,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
setMessage(string(buf));
#ifdef CVC4_DEBUG
- if(s_debugLastException == NULL) {
- // we leak buf[] but only in debug mode with assertions failing
- s_debugLastException = buf;
+ LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
+ if(buffer != NULL){
+ if(buffer->getContents() == NULL) {
+ buffer->setContents(buf);
+ }
}
-#else /* CVC4_DEBUG */
- delete [] buf;
#endif /* CVC4_DEBUG */
+ delete [] buf;
}
void IllegalArgumentException::construct(const char* header, const char* extra,
@@ -147,13 +171,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
setMessage(string(buf));
#ifdef CVC4_DEBUG
- if(s_debugLastException == NULL) {
- // we leak buf[] but only in debug mode with assertions failing
- s_debugLastException = buf;
+ LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
+ if(buffer != NULL){
+ if(buffer->getContents() == NULL) {
+ buffer->setContents(buf);
+ }
}
-#else /* CVC4_DEBUG */
- delete [] buf;
#endif /* CVC4_DEBUG */
+ delete [] buf;
}
} /* namespace CVC4 */
diff --git a/src/base/exception.h b/src/base/exception.h
index 84872b9b1..02384b6cb 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -27,6 +27,8 @@
#include <stdexcept>
#include <string>
+#include "base/tls.h"
+
namespace CVC4 {
class CVC4_PUBLIC Exception : public std::exception {
@@ -136,6 +138,30 @@ template <class T> inline void CheckArgument(bool cond, const T& arg) {
} \
}
+class CVC4_PUBLIC LastExceptionBuffer {
+public:
+ LastExceptionBuffer();
+ ~LastExceptionBuffer();
+
+ void setContents(const char* string);
+ const char* getContents() const { return d_contents; }
+
+ static LastExceptionBuffer* getCurrent() { return s_currentBuffer; }
+ static void setCurrent(LastExceptionBuffer* buffer) { s_currentBuffer = buffer; }
+
+ static const char* currentContents() {
+ return (getCurrent() == NULL) ? NULL : getCurrent()->getContents();
+ }
+
+private:
+ /* Disallow copies */
+ LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNUSED;
+ LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNUSED;
+
+ char* d_contents;
+
+ static CVC4_THREADLOCAL(LastExceptionBuffer*) s_currentBuffer;
+}; /* class LastExceptionBuffer */
}/* CVC4 namespace */
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 2b5c0a2c8..cf9a772b7 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -18,6 +18,7 @@
#include <iostream>
#include <cstring>
+#include "base/exception.h"
#include "base/output.h"
#include "expr/attribute.h"
@@ -31,8 +32,10 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
Exception(message),
d_node(new Node(node)) {
#ifdef CVC4_DEBUG
- // yes, this leaks memory, but only in debug modes with exceptions occurring
- s_debugLastException = strdup(toString().c_str());
+ LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
+ if(current != NULL){
+ current->setContents(toString().c_str());
+ }
#endif /* CVC4_DEBUG */
}
diff --git a/src/main/util.cpp b/src/main/util.cpp
index ce4e4509d..bc3d45287 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -44,7 +44,7 @@ using namespace std;
namespace CVC4 {
#ifdef CVC4_DEBUG
- extern CVC4_THREADLOCAL(const char*) s_debugLastException;
+//extern CVC4_THREADLOCAL(const char*) s_debugLastException;
#endif /* CVC4_DEBUG */
namespace main {
@@ -167,12 +167,14 @@ void cvc4unexpected() {
"CVC4 threw an \"unexpected\" exception (one that wasn't properly "
"specified\nin the throws() specifier for the throwing function)."
"\n\n");
- if(CVC4::s_debugLastException == NULL) {
+
+ const char* lastContents = LastExceptionBuffer::currentContents();
+
+ if(lastContents == NULL) {
fprintf(stderr,
"The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
} else {
- fprintf(stderr, "The exception is:\n%s\n\n",
- static_cast<const char*>(CVC4::s_debugLastException));
+ fprintf(stderr, "The exception is:\n%s\n\n", lastContents);
}
if(!segvSpin) {
if((*pOptions)[options::statistics] && pExecutor != NULL) {
@@ -201,6 +203,10 @@ void cvc4unexpected() {
void cvc4terminate() {
set_terminate(default_terminator);
#ifdef CVC4_DEBUG
+ LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
+ LastExceptionBuffer::setCurrent(NULL);
+ delete current;
+
fprintf(stderr, "\n"
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding. "
@@ -224,6 +230,10 @@ void cvc4terminate() {
/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */
void cvc4_init() throw(Exception) {
+#ifdef CVC4_DEBUG
+ LastExceptionBuffer::setCurrent(new LastExceptionBuffer());
+#endif
+
#ifndef __WIN32__
stack_t ss;
ss.ss_sp = malloc(SIGSTKSZ);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback