diff options
Diffstat (limited to 'src/util/Assert.cpp')
| -rw-r--r-- | src/util/Assert.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 8e2dd9220..f992032ee 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -25,6 +25,10 @@ using namespace std; namespace CVC4 { +#ifdef CVC4_DEBUG +__thread CVC4_PUBLIC const char* s_debugAssertionFailure = NULL; +#endif /* CVC4_DEBUG */ + void AssertionException::construct(const char* header, const char* extra, const char* function, const char* file, unsigned line, const char* fmt, @@ -65,7 +69,13 @@ 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 + s_debugAssertionFailure = buf; +#else /* CVC4_DEBUG */ delete [] buf; +#endif /* CVC4_DEBUG */ } void AssertionException::construct(const char* header, const char* extra, @@ -98,7 +108,13 @@ 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 + s_debugAssertionFailure = buf; +#else /* CVC4_DEBUG */ delete [] buf; +#endif /* CVC4_DEBUG */ } }/* CVC4 namespace */ |