diff options
Diffstat (limited to 'src/base/check.h')
-rw-r--r-- | src/base/check.h | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/src/base/check.h b/src/base/check.h index 91184336b..19329f14f 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -22,7 +22,7 @@ ** Assert is a AlwaysAssert that is only enabled in debug builds. ** Assert(pointer != nullptr); ** - ** CVC4_FATAL() can be used to indicate unreachable code. + ** CVC5_FATAL() can be used to indicate unreachable code. ** ** The AlwaysAssert and Assert macros are not safe for use in ** signal-handling code. In future, a a signal-handling safe version of @@ -40,39 +40,39 @@ #include "base/exception.h" #include "cvc4_export.h" -// Define CVC4_NO_RETURN macro replacement for [[noreturn]]. +// Define CVC5_NO_RETURN macro replacement for [[noreturn]]. #if defined(SWIG) -#define CVC4_NO_RETURN +#define CVC5_NO_RETURN // SWIG does not yet support [[noreturn]] so emit nothing instead. #else -#define CVC4_NO_RETURN [[noreturn]] +#define CVC5_NO_RETURN [[noreturn]] // Not checking for whether the compiler supports [[noreturn]] using // __has_cpp_attribute as GCC 4.8 is too widespread and does not support this. // We instead assume this is C++11 (or later) and [[noreturn]] is available. #endif // defined(SWIG) -// Define CVC4_PREDICT_FALSE(x) that helps the compiler predict that x will be +// Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be // false (if there is compiler support). #ifdef __has_builtin #if __has_builtin(__builtin_expect) -#define CVC4_PREDICT_FALSE(x) (__builtin_expect(x, false)) -#define CVC4_PREDICT_TRUE(x) (__builtin_expect(x, true)) +#define CVC5_PREDICT_FALSE(x) (__builtin_expect(x, false)) +#define CVC5_PREDICT_TRUE(x) (__builtin_expect(x, true)) #else -#define CVC4_PREDICT_FALSE(x) x -#define CVC4_PREDICT_TRUE(x) x +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x #endif #else -#define CVC4_PREDICT_FALSE(x) x -#define CVC4_PREDICT_TRUE(x) x +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x #endif #ifdef __has_cpp_attribute #if __has_cpp_attribute(fallthrough) -#define CVC4_FALLTHROUGH [[fallthrough]] +#define CVC5_FALLTHROUGH [[fallthrough]] #endif // __has_cpp_attribute(fallthrough) #endif // __has_cpp_attribute -#ifndef CVC4_FALLTHROUGH -#define CVC4_FALLTHROUGH +#ifndef CVC5_FALLTHROUGH +#define CVC5_FALLTHROUGH #endif namespace cvc5 { @@ -96,7 +96,7 @@ class CVC4_EXPORT FatalStream { public: FatalStream(const char* function, const char* file, int line); - CVC4_NO_RETURN ~FatalStream(); + CVC5_NO_RETURN ~FatalStream(); std::ostream& stream(); @@ -114,7 +114,7 @@ class OstreamVoider void operator&(std::ostream&) {} }; -// CVC4_FATAL() always aborts a function and provides a convenient way of +// CVC5_FATAL() always aborts a function and provides a convenient way of // formatting error messages. This can be used instead of a return type. // // Example function that returns a type Foo: @@ -122,13 +122,13 @@ class OstreamVoider // switch(t.type()) { // ... // default: -// CVC4_FATAL() << "Unknown T type " << t.enum(); +// CVC5_FATAL() << "Unknown T type " << t.enum(); // } // } -#define CVC4_FATAL() \ +#define CVC5_FATAL() \ FatalStream(__PRETTY_FUNCTION__, __FILE__, __LINE__).stream() -/* GCC <= 9.2 ignores CVC4_NO_RETURN of ~FatalStream() if +/* GCC <= 9.2 ignores CVC5_NO_RETURN of ~FatalStream() if * used in template classes (e.g., CDHashMap::save()). As a workaround we * explicitly call abort() to let the compiler know that the * corresponding function call will not return. */ @@ -137,8 +137,8 @@ class OstreamVoider // If `cond` is true, log an error message and abort the process. // Otherwise, does nothing. This leaves a hanging std::ostream& that can be // inserted into. -#define CVC4_FATAL_IF(cond, function, file, line) \ - CVC4_PREDICT_FALSE(!(cond)) \ +#define CVC5_FATAL_IF(cond, function, file, line) \ + CVC5_PREDICT_FALSE(!(cond)) \ ? (void)0 : OstreamVoider() & FatalStream(function, file, line).stream() // If `cond` is false, log an error message and abort()'s the process. @@ -149,16 +149,16 @@ class OstreamVoider // AlwaysAssert(x >= 0) << "expected a positive value. Got " << x << " // instead"; #define AlwaysAssert(cond) \ - CVC4_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ + CVC5_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ << "Check failure\n\n " << #cond << "\n" // Assert is a variant of AlwaysAssert() that is only checked when -// CVC4_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. -#ifdef CVC4_ASSERTIONS +// CVC5_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. +#ifdef CVC5_ASSERTIONS #define Assert(cond) AlwaysAssert(cond) #else #define Assert(cond) \ - CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) + CVC5_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) #endif class AssertArgumentException : public Exception @@ -197,13 +197,13 @@ class AssertArgumentException : public Exception }; /* class AssertArgumentException */ -#define Unreachable() CVC4_FATAL() << "Unreachable code reached" +#define Unreachable() CVC5_FATAL() << "Unreachable code reached" -#define Unhandled() CVC4_FATAL() << "Unhandled case encountered" +#define Unhandled() CVC5_FATAL() << "Unhandled case encountered" -#define Unimplemented() CVC4_FATAL() << "Unimplemented code encountered" +#define Unimplemented() CVC5_FATAL() << "Unimplemented code encountered" -#define InternalError() CVC4_FATAL() << "Internal error detected" +#define InternalError() CVC5_FATAL() << "Internal error detected" #define IllegalArgument(arg, msg...) \ throw ::cvc5::IllegalArgumentException( \ @@ -235,15 +235,15 @@ class AssertArgumentException : public Exception } \ } while (0) -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS #define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ##msg) #define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ##msg) -#else /* ! CVC4_ASSERTIONS */ +#else /* ! CVC5_ASSERTIONS */ #define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \ )*/ #define DebugCheckArgument( \ cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/ -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ } // namespace cvc5 |