From 9d5bc024e4b1500e328fe69c83b58f78e8df69b6 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 5 Feb 2015 09:51:05 +0000 Subject: [PATCH] add implementation of UNREACHABLE for MSVC in release mode. This reduces code size of Z3 by 0.1% \o/ Signed-off-by: Nuno Lopes --- src/util/debug.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/debug.h b/src/util/debug.h index a36743f73..f7383511b 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -58,12 +58,18 @@ bool is_debug_enabled(const char * tag); #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); }) +#ifdef Z3DEBUG +# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();) +#else #if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable) // only available in gcc >= 4.5 and in newer versions of clang # define UNREACHABLE() __builtin_unreachable() +#elif defined(_MSC_VER) +# define UNREACHABLE() __assume(0) #else #define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();) #endif +#endif #define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)