diff options
Diffstat (limited to 'src/base/check.cpp')
-rw-r--r-- | src/base/check.cpp | 212 |
1 files changed, 212 insertions, 0 deletions
diff --git a/src/base/check.cpp b/src/base/check.cpp new file mode 100644 index 000000000..10ecad191 --- /dev/null +++ b/src/base/check.cpp @@ -0,0 +1,212 @@ +/********************* */ +/*! \file check.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Assertion utility classes, functions and macros. + ** + ** Implementation of assertion utility classes, functions and macros. + **/ + +#include "base/check.h" + +#include <cstdlib> +#include <iostream> + +namespace CVC4 { + +FatalStream::FatalStream(const char* function, const char* file, int line) +{ + stream() << "Fatal failure within " << function << " at " << file << ":" + << line << "\n"; +} + +FatalStream::~FatalStream() +{ + Flush(); + abort(); +} + +std::ostream& FatalStream::stream() { return std::cerr; } + +void FatalStream::Flush() +{ + stream() << std::endl; + stream().flush(); +} + +void AssertArgumentException::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 = 512; + char* buf; + buf = new char[n]; + + for (;;) + { + 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_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; + buf = new char[n]; + } + } + + setMessage(std::string(buf)); + +#ifdef CVC4_DEBUG + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if (buffer != NULL) + { + if (buffer->getContents() == NULL) + { + buffer->setContents(buf); + } + } +#endif /* CVC4_DEBUG */ + delete[] buf; +} + +void AssertArgumentException::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(std::string(buf)); + +#ifdef CVC4_DEBUG + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if (buffer != NULL) + { + if (buffer->getContents() == NULL) + { + buffer->setContents(buf); + } + } +#endif /* CVC4_DEBUG */ + delete[] buf; +} + +AssertArgumentException::AssertArgumentException(const char* condStr, + const char* argDesc, + const char* function, + const char* file, + unsigned line, + const char* fmt, + ...) + : Exception() +{ + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + (std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold") + .c_str(), + function, + file, + line, + fmt, + args); + va_end(args); +} + +AssertArgumentException::AssertArgumentException(const char* condStr, + const char* argDesc, + const char* function, + const char* file, + unsigned line) + : Exception() +{ + construct("Illegal argument detected", + (std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold") + .c_str(), + function, + file, + line); +} + +} // namespace CVC4 |