Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape to user space

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

4 files changed, 14 insertions, 14 deletions

diff --git a/src/util/cvc4_assert.cpp b/src/util/cvc4_assert.cpp
index eb7b81a39..08e2867f6 100644
--- a/src/util/cvc4_assert.cpp
+++ b/src/util/cvc4_assert.cpp
@@ -136,7 +136,7 @@ void debugAssertionFailed(const AssertionException& thisException,
                           const char* propagatingException) {
   static CVC4_THREADLOCAL(bool) alreadyFired = false;
 
-  if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) {
+  if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
     throw thisException;
   }
 
diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h
index c070fc389..7d359a56b 100644
--- a/src/util/cvc4_assert.h
+++ b/src/util/cvc4_assert.h
@@ -252,7 +252,7 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 // details of the exception
 #  define AlwaysAssert(cond, msg...)                                    \
     do {                                                                \
-      if(EXPECT_FALSE( ! (cond) )) {                                    \
+      if(__builtin_expect( ( ! (cond) ), false )) {                                    \
         /* save the last assertion failure */                           \
         const char* lastException = ::CVC4::s_debugLastException;       \
         ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
@@ -265,7 +265,7 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 // will terminate() if thrown during stack unwinding.
 #  define AlwaysAssert(cond, msg...)                                    \
      do {                                                               \
-       if(EXPECT_FALSE( ! (cond) )) {                                   \
+       if(__builtin_expect( ( ! (cond) ), false )) {                                   \
          throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
        }                                                                \
      } while(0)
@@ -283,13 +283,13 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
   throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
   do { \
-    if(EXPECT_FALSE( ! (cond) )) { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
       throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
     } \
   } while(0)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
   do { \
-    if(EXPECT_FALSE( ! (cond) )) { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
       throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
     } \
   } while(0)
@@ -299,9 +299,9 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 #  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...) /*EXPECT_TRUE( cond )*/
-#  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
-#  define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
+#  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 */
diff --git a/src/util/debug.h b/src/util/debug.h
index 3e7c4d8be..97c176f02 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -27,11 +27,11 @@
 
 #ifdef CVC4_ASSERTIONS
 // the __builtin_expect() helps us if assert is built-in or a macro
-#  define cvc4assert(x) assert(EXPECT_TRUE( x ))
+#  define cvc4assert(x) assert(__builtin_expect( ( x ), true ))
 #else
 // TODO: use a compiler annotation when assertions are off ?
 // (to improve optimization)
-#  define cvc4assert(x) /*EXPECT_TRUE( x )*/
+#  define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
 #endif /* CVC4_ASSERTIONS */
 
 #endif /* __CVC4__DEBUG_H */
diff --git a/src/util/exception.h b/src/util/exception.h
index 082a50ef2..cd4b763ef 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -138,13 +138,13 @@ namespace CVC4 {
 #ifndef CheckArgument
 template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
 template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
 template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
 template <class T> inline void CheckArgument(bool cond, const T& arg) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
@@ -153,13 +153,13 @@ template <class T> inline void CheckArgument(bool cond, const T& arg) {
 #ifndef DebugCheckArgument
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
 template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
-  if(EXPECT_FALSE( !cond )) { \
+  if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }