mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
parent
a951ff0769
commit
0e387b2abe
|
@ -516,7 +516,7 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v
|
|||
switch (size) {
|
||||
case 2:
|
||||
b += array[1]->hash();
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 1:
|
||||
c += array[0]->hash();
|
||||
}
|
||||
|
|
|
@ -1500,7 +1500,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
|
|||
result = m_util.mk_bv_not(new_args[1]);
|
||||
return BR_DONE;
|
||||
}
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
default:
|
||||
if (m_bv_sort_ac)
|
||||
std::sort(new_args.begin(), new_args.end(), ast_to_lt());
|
||||
|
|
|
@ -67,7 +67,7 @@ namespace smt {
|
|||
switch (num_args) {
|
||||
case 2:
|
||||
b += arg_hash(n, 1);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 1:
|
||||
c += arg_hash(n, 0);
|
||||
}
|
||||
|
|
|
@ -127,7 +127,7 @@ namespace smt {
|
|||
switch (i) {
|
||||
case 2:
|
||||
b += n->get_arg(1)->get_root()->hash();
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 1:
|
||||
c += n->get_arg(0)->get_root()->hash();
|
||||
}
|
||||
|
|
|
@ -52,38 +52,38 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) {
|
|||
switch(len) { /* all the case statements fall through */
|
||||
case 11:
|
||||
c+=((unsigned)str[10]<<24);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 10:
|
||||
c+=((unsigned)str[9]<<16);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 9 :
|
||||
c+=((unsigned)str[8]<<8);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
/* the first byte of c is reserved for the length */
|
||||
case 8 :
|
||||
b+=((unsigned)str[7]<<24);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 7 :
|
||||
b+=((unsigned)str[6]<<16);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 6 :
|
||||
b+=((unsigned)str[5]<<8);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 5 :
|
||||
b+=str[4];
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 4 :
|
||||
a+=((unsigned)str[3]<<24);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 3 :
|
||||
a+=((unsigned)str[2]<<16);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 2 :
|
||||
a+=((unsigned)str[1]<<8);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 1 :
|
||||
a+=str[0];
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
/* case 0: nothing left to add */
|
||||
}
|
||||
mix(a,b,c);
|
||||
|
|
|
@ -22,10 +22,6 @@ Revision History:
|
|||
#include<algorithm>
|
||||
#include"util.h"
|
||||
|
||||
#ifndef __fallthrough
|
||||
#define __fallthrough
|
||||
#endif
|
||||
|
||||
#define mix(a,b,c) \
|
||||
{ \
|
||||
a -= b; a -= c; a ^= (c>>13); \
|
||||
|
@ -116,7 +112,7 @@ unsigned get_composite_hash(Composite app, unsigned n, GetKindHashProc const & k
|
|||
switch (n) {
|
||||
case 2:
|
||||
b += chasher(app, 1);
|
||||
__fallthrough;
|
||||
Z3_fallthrough;
|
||||
case 1:
|
||||
c += chasher(app, 0);
|
||||
}
|
||||
|
|
|
@ -68,6 +68,18 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8);
|
|||
#define THREAD_LOCAL
|
||||
#endif
|
||||
|
||||
#ifdef __fallthrough
|
||||
# define Z3_fallthrough __fallthrough
|
||||
#elif defined(__has_cpp_attribute)
|
||||
# if __has_cpp_attribute(clang::fallthrough)
|
||||
# define Z3_fallthrough [[clang::fallthrough]]
|
||||
# else
|
||||
# define Z3_fallthrough
|
||||
# endif
|
||||
#else
|
||||
# define Z3_fallthrough
|
||||
#endif
|
||||
|
||||
inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
|
||||
|
||||
/**
|
||||
|
@ -273,10 +285,6 @@ bool has_duplicates(const IT & begin, const IT & end) {
|
|||
return false;
|
||||
}
|
||||
|
||||
#ifndef __fallthrough
|
||||
#define __fallthrough
|
||||
#endif
|
||||
|
||||
#ifndef _WINDOWS
|
||||
#ifndef __declspec
|
||||
#define __declspec(X)
|
||||
|
|
Loading…
Reference in a new issue