diff options
Diffstat (limited to 'src/util/cvc4_assert.h')
-rw-r--r-- | src/util/cvc4_assert.h | 309 |
1 files changed, 0 insertions, 309 deletions
diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h deleted file mode 100644 index cc854278b..000000000 --- a/src/util/cvc4_assert.h +++ /dev/null @@ -1,309 +0,0 @@ -/********************* */ -/*! \file cvc4_assert.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): ACSYS - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Assertion utility classes, functions, exceptions, and macros. - ** - ** Assertion utility classes, functions, exceptions, and macros. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__ASSERT_H -#define __CVC4__ASSERT_H - -#include <string> -#include <sstream> -#include <cstdio> -#include <cstdlib> -#include <cstdarg> - -#include "util/exception.h" -#include "util/tls.h" - -// output.h not strictly needed for this header, but it _is_ needed to -// actually _use_ anything in this header, so let's include it. -#include "util/output.h" - -namespace CVC4 { - -class AssertionException : public Exception { -protected: - void construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line, const char* fmt, ...) { - va_list args; - va_start(args, fmt); - construct(header, extra, function, file, line, fmt, args); - va_end(args); - } - - void construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line, const char* fmt, va_list args); - - void construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line); - - AssertionException() : Exception() {} - -public: - AssertionException(const char* extra, const char* function, - const char* file, unsigned line, - const char* fmt, ...) : - Exception() { - va_list args; - va_start(args, fmt); - construct("Assertion failure", extra, function, file, line, fmt, args); - va_end(args); - } - - AssertionException(const char* extra, const char* function, - const char* file, unsigned line) : - Exception() { - construct("Assertion failure", extra, function, file, line); - } -};/* class AssertionException */ - -class UnreachableCodeException : public AssertionException { -protected: - UnreachableCodeException() : AssertionException() {} - -public: - UnreachableCodeException(const char* function, const char* file, - unsigned line, const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Unreachable code reached", - NULL, function, file, line, fmt, args); - va_end(args); - } - - UnreachableCodeException(const char* function, const char* file, - unsigned line) : - AssertionException() { - construct("Unreachable code reached", NULL, function, file, line); - } -};/* class UnreachableCodeException */ - -class UnhandledCaseException : public UnreachableCodeException { -protected: - UnhandledCaseException() : UnreachableCodeException() {} - -public: - UnhandledCaseException(const char* function, const char* file, - unsigned line, const char* fmt, ...) : - UnreachableCodeException() { - va_list args; - va_start(args, fmt); - construct("Unhandled case encountered", - NULL, function, file, line, fmt, args); - va_end(args); - } - - template <class T> - UnhandledCaseException(const char* function, const char* file, - unsigned line, T theCase) : - UnreachableCodeException() { - std::stringstream sb; - sb << theCase; - construct("Unhandled case encountered", - NULL, function, file, line, "The case was: %s", sb.str().c_str()); - } - - UnhandledCaseException(const char* function, const char* file, - unsigned line) : - UnreachableCodeException() { - construct("Unhandled case encountered", NULL, function, file, line); - } -};/* class UnhandledCaseException */ - -class UnimplementedOperationException : public AssertionException { -protected: - UnimplementedOperationException() : AssertionException() {} - -public: - UnimplementedOperationException(const char* function, const char* file, - unsigned line, const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Unimplemented code encountered", - NULL, function, file, line, fmt, args); - va_end(args); - } - - UnimplementedOperationException(const char* function, const char* file, - unsigned line) : - AssertionException() { - construct("Unimplemented code encountered", NULL, function, file, line); - } -};/* class UnimplementedOperationException */ - -class AssertArgumentException : public AssertionException { -protected: - AssertArgumentException() : AssertionException() {} - -public: - AssertArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line, - const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), - function, file, line, fmt, args); - va_end(args); - } - - AssertArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line) : - AssertionException() { - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), - function, file, line); - } - - AssertArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line, const char* fmt, ...) : - AssertionException() { - 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(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line) : - AssertionException() { - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument; expected " + - condStr + " to hold" ).c_str(), - function, file, line); - } -};/* class AssertArgumentException */ - -class InternalErrorException : public AssertionException { -protected: - InternalErrorException() : AssertionException() {} - -public: - InternalErrorException(const char* function, const char* file, unsigned line) : - AssertionException() { - construct("Internal error detected", "", - function, file, line); - } - - InternalErrorException(const char* function, const char* file, unsigned line, - const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Internal error detected", "", - function, file, line, fmt, args); - va_end(args); - } - - InternalErrorException(const char* function, const char* file, unsigned line, - std::string fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Internal error detected", "", - function, file, line, fmt.c_str(), args); - va_end(args); - } - -};/* class InternalErrorException */ - -#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 - * additional logic so as not to bloat the code at every Assert() - * expansion. - * - * Note this name is prefixed with "debug" because it is included in - * debug builds only; in debug builds, it handles all assertion - * failures (even those that exist in non-debug builds). - */ -void debugAssertionFailed(const AssertionException& thisException, const char* lastException); - -// If we're currently handling an exception, print a warning instead; -// otherwise std::terminate() is called by the runtime and we lose -// details of the exception -# define AlwaysAssert(cond, msg...) \ - do { \ - if(__builtin_expect( ( ! (cond) ), false )) { \ - /* save the last assertion failure */ \ - const char* lastException = ::CVC4::s_debugLastException; \ - ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - ::CVC4::debugAssertionFailed(exception, lastException); \ - } \ - } while(0) - -#else /* CVC4_DEBUG */ -// These simpler (but less useful) versions for non-debug builds fails -// will terminate() if thrown during stack unwinding. -# define AlwaysAssert(cond, msg...) \ - do { \ - if(__builtin_expect( ( ! (cond) ), false )) { \ - throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - } \ - } while(0) -#endif /* CVC4_DEBUG */ - -#define Unreachable(msg...) \ - throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define Unhandled(msg...) \ - throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define Unimplemented(msg...) \ - throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define InternalError(msg...) \ - throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define IllegalArgument(arg, msg...) \ - throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) -#define CheckArgument(cond, arg, msg...) \ - do { \ - if(__builtin_expect( ( ! (cond) ), false )) { \ - throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ - } \ - } while(0) -#define AlwaysAssertArgument(cond, arg, msg...) \ - do { \ - if(__builtin_expect( ( ! (cond) ), false )) { \ - throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - } \ - } while(0) - -#ifdef CVC4_ASSERTIONS -# define Assert(cond, msg...) AlwaysAssert(cond, ## msg) -# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) -# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg) -#else /* ! CVC4_ASSERTIONS */ -# define Assert(cond, msg...) /*__builtin_expect( ( cond ), true )*/ -# define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/ -# define DebugCheckArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/ -#endif /* CVC4_ASSERTIONS */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__ASSERT_H */ |