diff options
author | Tim King <taking@cs.nyu.edu> | 2018-02-09 12:34:47 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-09 14:34:47 -0600 |
commit | a7f08481352ea1c45091b681e990ccc513ae175f (patch) | |
tree | 76eabd2efdce313cde9aed1e9eb0be7e1c310b93 /src/base | |
parent | d4b136c10ac3a226061d12cdf8e12340ad0a974d (diff) |
Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertion macros. This name is likely temporary while Assert() is deprecated. (#1590)
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/cvc4_check.h | 48 |
1 files changed, 25 insertions, 23 deletions
diff --git a/src/base/cvc4_check.h b/src/base/cvc4_check.h index fb4ec0bba..5cb3315f4 100644 --- a/src/base/cvc4_check.h +++ b/src/base/cvc4_check.h @@ -11,24 +11,25 @@ ** ** \brief Assertion utility classes, functions and macros. ** - ** The CHECK utility classes, functions and macros are related to the Assert() - ** macros defined in base/cvc4_assert.h. The major distinguishing attribute - ** is the CHECK's abort() the process on failures while Assert() statements - ** throw C++ exceptions. + ** The CVC4_CHECK utility classes, functions and macros are related to the + ** Assert() macros defined in base/cvc4_assert.h. The major distinguishing + ** attribute is the CVC4_CHECK's abort() the process on failures while + ** Assert() statements throw C++ exceptions. ** - ** The main usage in the file is the CHECK macros. The CHECK macros assert a - ** condition and aborts()'s the process if the condition is not satisfied. The - ** macro leaves a hanging ostream for the user to specify additional - ** information about the failure. Example usage: - ** CHECK(x >= 0) << "x must be positive."; + ** The main usage in the file is the CVC4_CHECK macros. The CVC4_CHECK macros + ** assert a condition and aborts()'s the process if the condition is not + ** satisfied. The macro leaves a hanging ostream for the user to specify + ** additional information about the failure. Example usage: + ** CVC4_CHECK(x >= 0) << "x must be positive."; ** - ** DCHECK is a CHECK that is only enabled in debug builds. - ** DCHECK(pointer != nullptr); + ** CVC4_DCHECK is a CVC4_CHECK that is only enabled in debug builds. + ** CVC4_DCHECK(pointer != nullptr); ** ** CVC4_FATAL() can be used to indicate unreachable code. ** - ** The CHECK and DCHECK macros are not safe for use in signal-handling code. - ** TODO(taking): Add a signal-handling safe version of CHECK. + ** The CVC4_CHECK and CVC4_DCHECK macros are not safe for use in + ** signal-handling code. In future, a a signal-handling safe version of + ** CVC4_CHECK may be added. **/ #include "cvc4_private.h" @@ -65,10 +66,11 @@ namespace CVC4 { // Implementation notes: // To understand FatalStream and OStreamVoider, it is useful to understand -// how a CHECK is structured. CHECK(cond) is roughly the following pattern: +// how a CVC4_CHECK is structured. CVC4_CHECK(cond) is roughly the following +// pattern: // cond ? (void)0 : OstreamVoider() & FatalStream().stream() // This is a carefully crafted message to achieve a hanging ostream using -// operator precedence. The line `CHECK(cond) << foo << bar;` will bind as +// operator precedence. The line `CVC4_CHECK(cond) << foo << bar;` will bind as // follows: // `cond ? ((void)0) : (OSV() & ((FS().stream() << foo) << bar));` // Once the expression is evaluated, the destructor ~FatalStream() of the @@ -123,19 +125,19 @@ class OstreamVoider // If `cond` is false, log an error message and abort()'s the process. // Otherwise, does nothing. This leaves a hanging std::ostream& that can be // inserted into using operator<<. Example usages: -// CHECK(x >= 0); -// CHECK(x >= 0) << "x must be positive"; -// CHECK(x >= 0) << "expected a positive value. Got " << x << " instead"; -#define CHECK(cond) \ +// CVC4_CHECK(x >= 0); +// CVC4_CHECK(x >= 0) << "x must be positive"; +// CVC4_CHECK(x >= 0) << "expected a positive value. Got " << x << " instead"; +#define CVC4_CHECK(cond) \ CVC4_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ << "Check failure\n\n " << #cond << "\n" -// DCHECK is a variant of CHECK() that is only checked when CVC4_ASSERTIONS is -// defined. We rely on the optimizer to remove the deadcode. +// CVC4_DCHECK is a variant of CVC4_CHECK() that is only checked when +// CVC4_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. #ifdef CVC4_ASSERTIONS -#define DCHECK(cond) CHECK(cond) +#define CVC4_DCHECK(cond) CVC4_CHECK(cond) #else -#define DCHECK(cond) \ +#define CVC4_DCHECK(cond) \ CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) #endif /* CVC4_DEBUG */ |