diff options
Diffstat (limited to 'src/util/assert.h')
-rw-r--r-- | src/util/assert.h | 76 |
1 files changed, 67 insertions, 9 deletions
diff --git a/src/util/assert.h b/src/util/assert.h index 24e3a4cdf..6691c1b04 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -7,20 +7,78 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Assertion utility classes, functions, and exceptions. **/ #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H -#include <cassert> +#include <string> +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" -#ifdef DEBUG -// the __builtin_expect() helps us if assert is built-in or a macro -# define cvc4assert(x) assert(__builtin_expect((x), 1)) -#else -// TODO: use a compiler annotation when assertions are off ? -// (to improve optimization) -# define cvc4assert(x) -#endif /* DEBUG */ +namespace CVC4 { + +class AssertionException : public Exception { +public: + AssertionException() : Exception() {} + AssertionException(std::string msg) : Exception(msg) {} + AssertionException(const char* msg) : Exception(msg) {} +};/* class AssertionException */ + +class UnreachableCodeException : public AssertionException { +public: + UnreachableCodeException() : AssertionException() {} + UnreachableCodeException(std::string msg) : AssertionException(msg) {} + UnreachableCodeException(const char* msg) : AssertionException(msg) {} +};/* class UnreachableCodeException */ + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg) + +#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) +#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg) + +inline void AssertImpl(const char* info, bool cond, std::string msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond, const char* msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(info); +} + +#ifdef __GNUC__ +inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnreachableImpl(const char* info, std::string msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info, const char* msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info) { + throw new UnreachableCodeException(info); +} + +}/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ |