#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
-#include <string>
-#include <sstream>
+#include <cstdarg>
#include <cstdio>
#include <cstdlib>
-#include <cstdarg>
+#include <sstream>
+#include <string>
#include "base/exception.h"
#include "base/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.
// Tim : Disabling this and moving it into cvc4_assert.cpp
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, ...) {
+ 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, const char* fmt,
+ va_list args);
- void construct(const char* header, const char* extra,
- const char* function, const char* file,
- unsigned line);
+ 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() {
+ 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() {
+ AssertionException(const char* extra, const char* function, const char* file,
+ unsigned line)
+ : Exception() {
construct("Assertion failure", extra, function, file, line);
}
-};/* class AssertionException */
+}; /* class AssertionException */
class UnreachableCodeException : public AssertionException {
-protected:
+ protected:
UnreachableCodeException() : AssertionException() {}
-public:
+ public:
UnreachableCodeException(const char* function, const char* file,
- unsigned line, const char* fmt, ...) :
- AssertionException() {
+ unsigned line, const char* fmt, ...)
+ : AssertionException() {
va_list args;
va_start(args, fmt);
- construct("Unreachable code reached",
- NULL, function, file, line, fmt, args);
+ construct("Unreachable code reached", NULL, function, file, line, fmt,
+ args);
va_end(args);
}
UnreachableCodeException(const char* function, const char* file,
- unsigned line) :
- AssertionException() {
+ unsigned line)
+ : AssertionException() {
construct("Unreachable code reached", NULL, function, file, line);
}
-};/* class UnreachableCodeException */
+}; /* class UnreachableCodeException */
class UnhandledCaseException : public UnreachableCodeException {
-protected:
+ protected:
UnhandledCaseException() : UnreachableCodeException() {}
-public:
- UnhandledCaseException(const char* function, const char* file,
- unsigned line, const char* fmt, ...) :
- 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);
+ 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() {
+ 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());
+ 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() {
+ UnhandledCaseException(const char* function, const char* file, unsigned line)
+ : UnreachableCodeException() {
construct("Unhandled case encountered", NULL, function, file, line);
}
-};/* class UnhandledCaseException */
+}; /* class UnhandledCaseException */
class UnimplementedOperationException : public AssertionException {
-protected:
+ protected:
UnimplementedOperationException() : AssertionException() {}
-public:
+ public:
UnimplementedOperationException(const char* function, const char* file,
- unsigned line, const char* fmt, ...) :
- AssertionException() {
+ unsigned line, const char* fmt, ...)
+ : AssertionException() {
va_list args;
va_start(args, fmt);
- construct("Unimplemented code encountered",
- NULL, function, file, line, fmt, args);
+ construct("Unimplemented code encountered", NULL, function, file, line, fmt,
+ args);
va_end(args);
}
UnimplementedOperationException(const char* function, const char* file,
- unsigned line) :
- AssertionException() {
+ unsigned line)
+ : AssertionException() {
construct("Unimplemented code encountered", NULL, function, file, line);
}
-};/* class UnimplementedOperationException */
+}; /* class UnimplementedOperationException */
class AssertArgumentException : public AssertionException {
-protected:
+ protected:
AssertArgumentException() : AssertionException() {}
-public:
+ public:
AssertArgumentException(const char* argDesc, const char* function,
- const char* file, unsigned line,
- const char* fmt, ...) :
- AssertionException() {
+ 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(),
+ (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() {
+ const char* file, unsigned line)
+ : AssertionException() {
construct("Illegal argument detected",
- ( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
+ (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() {
+ 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(),
+ (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() {
+ 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(),
+ (std::string("`") + argDesc + "' is a bad argument; expected " +
+ condStr + " to hold")
+ .c_str(),
function, file, line);
}
-};/* class AssertArgumentException */
+}; /* class AssertArgumentException */
class InternalErrorException : public AssertionException {
-protected:
+ protected:
InternalErrorException() : AssertionException() {}
-public:
- InternalErrorException(const char* function, const char* file, unsigned line) :
- AssertionException() {
- construct("Internal error detected", "",
- function, file, line);
+ 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() {
+ const char* fmt, ...)
+ : AssertionException() {
va_list args;
va_start(args, fmt);
- construct("Internal error detected", "",
- function, file, line, fmt, args);
+ 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() {
+ std::string fmt, ...)
+ : AssertionException() {
va_list args;
va_start(args, fmt);
- construct("Internal error detected", "",
- function, file, line, fmt.c_str(), args);
+ construct("Internal error detected", "", function, file, line, fmt.c_str(),
+ args);
va_end(args);
}
-};/* class InternalErrorException */
+}; /* class InternalErrorException */
#ifdef CVC4_DEBUG
* 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);
+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)
+#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)
+#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());
+#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)
+#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 */
+#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 */
projects / cvc5.git / commitdiff