summaryrefslogtreecommitdiff
path: root/src/base/cvc4_assert.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/cvc4_assert.h')
-rw-r--r--src/base/cvc4_assert.h320
1 files changed, 0 insertions, 320 deletions
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
deleted file mode 100644
index a29e6f545..000000000
--- a/src/base/cvc4_assert.h
+++ /dev/null
@@ -1,320 +0,0 @@
-/********************* */
-/*! \file cvc4_assert.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, 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, exceptions, and macros.
- **
- ** Assertion utility classes, functions, exceptions, and macros.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__ASSERT_H
-#define CVC4__ASSERT_H
-
-#include <cstdarg>
-#include <cstdio>
-#include <cstdlib>
-#include <sstream>
-#include <string>
-
-#include "base/exception.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.
-// Tim : Disabling this and moving it into cvc4_assert.cpp
-//#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
-
-/**
- * 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 */ \
- ::CVC4::LastExceptionBuffer* buffer = \
- ::CVC4::LastExceptionBuffer::getCurrent(); \
- const char* lastException = \
- (buffer == NULL) ? NULL : buffer->getContents(); \
- ::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__, \
- ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str());
-// This cannot use check argument directly as this forces
-// CheckArgument to use a va_list. This is unsupported in Swig.
-#define PrettyCheckArgument(cond, arg, msg...) \
- do { \
- if (__builtin_expect((!(cond)), false)) { \
- throw ::CVC4::IllegalArgumentException( \
- #cond, #arg, __PRETTY_FUNCTION__, \
- ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
- } \
- } 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback