summaryrefslogtreecommitdiff
path: root/src/util/cvc4_assert.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/cvc4_assert.h')
-rw-r--r--src/util/cvc4_assert.h309
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback