diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/util/exception.cpp | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/util/exception.cpp')
-rw-r--r-- | src/util/exception.cpp | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/src/util/exception.cpp b/src/util/exception.cpp new file mode 100644 index 000000000..d31f52fe7 --- /dev/null +++ b/src/util/exception.cpp @@ -0,0 +1,102 @@ +/********************* */ +/*! \file exception.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 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.\endverbatim + ** + ** \brief CVC4's exception base class and some associated utilities + ** + ** CVC4's exception base class and some associated utilities. + **/ + +#include "util/exception.h" +#include <string> +#include <cstdio> +#include <cstdlib> +#include <cstdarg> + +using namespace std; +using namespace CVC4; + +void IllegalArgumentException::construct(const char* header, const char* extra, + const char* function, 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 = 512; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n", + header, function); + } else { + size = snprintf(buf, n, "%s\n%s\n\n %s\n", + header, function, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args_copy); + 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 IllegalArgumentException::construct(const char* header, const char* extra, + const char* function) { + // 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", + header, function); + } else { + size = snprintf(buf, n, "%s.\n%s\n\n %s\n", + header, function, 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; +} |