3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-11 00:11:48 +00:00

Add a default back in for a case where gcc (erroneously) claims

control flow reaches end without return.  Must also locally disable the
clang covered-switch-default warning.
This commit is contained in:
David Detlefs 2026-08-08 09:44:08 -07:00
parent 00245058f0
commit 8766b939f1
2 changed files with 18 additions and 0 deletions

View file

@ -21,6 +21,7 @@ Revision History:
#include<ostream>
#include "util/debug.h"
#include "util/manage_warnings.h"
enum ext_numeral_kind { EN_MINUS_INFINITY, EN_NUMERAL, EN_PLUS_INFINITY };
@ -280,6 +281,16 @@ bool lt(numeral_manager & m,
return m.lt(a, b);
case EN_PLUS_INFINITY:
return true;
// The default case below is not necessary: the cases above cover all the
// elements of the ext_numeral_kind enum. But gcc complains with a warning
// if this default case is absent. So we leave it in, but disable Clang's
// (correct) warning that the default is unnecessary.
START_DISABLE_COVERED_SWITCH_DEFAULT;
default:
UNREACHABLE();
return false;
END_DISABLE_WARNING_STMT;
}
case EN_PLUS_INFINITY:
return false;

View file

@ -42,15 +42,22 @@ Revision History:
DO_PRAGMA(clang diagnostic ignored #s)
// This version should be used in decl contexts.
#define END_DISABLE_WARNING \
_Pragma("clang diagnostic pop") \
DUMMY_DECL
// This version should be used in statement contexts.
#define END_DISABLE_WARNING_STMT \
_Pragma("clang diagnostic pop")
#define START_DISABLE_EXTRA_SEMI_WARNING START_DISABLE_WARNING(-Wextra-semi)
#define START_DISABLE_COVERED_SWITCH_DEFAULT START_DISABLE_WARNING(-Wcovered-switch-default)
#else
#define START_DISABLE_EXTRA_SEMI_WARNING
#define START_DISABLE_COVERED_SWITCH_DEFAULT
#define END_DISABLE_WARNING
#endif