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