diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-09 23:14:40 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-09 23:14:40 +0000 |
commit | 2f121daa042c6f25a3f9ed8ece60ac5dccb11976 (patch) | |
tree | 58ee28d73e8638b100abe09e961bc3dbdf9d79d9 /src/util/Assert.cpp | |
parent | d697d1e91be226339a28bd7e8dce3862901cba8a (diff) |
some fixes and organizational adjustments to assert code, parsers/lexers, and build process
Diffstat (limited to 'src/util/Assert.cpp')
-rw-r--r-- | src/util/Assert.cpp | 101 |
1 files changed, 101 insertions, 0 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp new file mode 100644 index 000000000..799af12ab --- /dev/null +++ b/src/util/Assert.cpp @@ -0,0 +1,101 @@ +/********************* -*- C++ -*- */ +/** Assert.cpp + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Assertion utility classes, functions, and exceptions. Implementation. + **/ + +#include <new> +#include <cstdarg> +#include <cstdio> +#include "util/Assert.h" +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" + +using namespace std; + +namespace CVC4 { + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, + va_list args) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args); + va_end(args_copy); + + if(size < n) { + break; + } + } + + if(size >= n) { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + delete [] buf; +} + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + break; + } else { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + delete [] buf; +} + +}/* CVC4 namespace */ |