From a7f08481352ea1c45091b681e990ccc513ae175f Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 9 Feb 2018 12:34:47 -0800 Subject: [PATCH] Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertion macros. This name is likely temporary while Assert() is deprecated. (#1590) --- src/base/cvc4_check.h | 48 +++++++++++++++++--------------- src/util/statistics_registry.cpp | 11 ++++---- test/unit/util/check_white.h | 8 +++--- 3 files changed, 35 insertions(+), 32 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 */ diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 2dd1eddd7..b9f6998d4 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -77,7 +77,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - DCHECK(nsec >= 0 && nsec < nsec_per_sec); + CVC4_DCHECK(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -168,9 +168,10 @@ void StatisticsRegistry::registerStat(Stat* s) void StatisticsRegistry::unregisterStat(Stat* s) { #ifdef CVC4_STATISTICS_ON - CHECK(s != nullptr); - CHECK(d_stats.erase(s) > 0) << "Statistic `" << s->getName() - << "' was not registered with this registry."; + CVC4_CHECK(s != nullptr); + CVC4_CHECK(d_stats.erase(s) > 0) + << "Statistic `" << s->getName() + << "' was not registered with this registry."; #endif /* CVC4_STATISTICS_ON */ } /* StatisticsRegistry::unregisterStat() */ @@ -202,7 +203,7 @@ void TimerStat::start() { void TimerStat::stop() { if(__CVC4_USE_STATISTICS) { - CHECK(d_running) << "timer not running"; + CVC4_CHECK(d_running) << "timer not running"; ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; diff --git a/test/unit/util/check_white.h b/test/unit/util/check_white.h index e57afa6c7..b0c540265 100644 --- a/test/unit/util/check_white.h +++ b/test/unit/util/check_white.h @@ -39,19 +39,19 @@ class CheckWhite : public CxxTest::TestSuite "return type."; } - void testCheck() { CHECK(kOne >= 0) << kOne << " must be positive"; } + void testCheck() { CVC4_CHECK(kOne >= 0) << kOne << " must be positive"; } void testDCheck() { - DCHECK(kOne == 1) << "always passes"; + CVC4_DCHECK(kOne == 1) << "always passes"; #ifndef CVC4_ASSERTIONS - DCHECK(false) << "Will not be compiled in when CVC4_ASSERTIONS off."; + CVC4_DCHECK(false) << "Will not be compiled in when CVC4_ASSERTIONS off."; #endif /* CVC4_ASSERTIONS */ } void testPointerTypeCanBeTheCondition() { const int* one_pointer = &kOne; - CHECK(one_pointer); + CVC4_CHECK(one_pointer); } }; -- 2.30.2