diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp index 1a25d177b0d..781aef5aebe 100644 --- a/regression/invariants/driver.cpp +++ b/regression/invariants/driver.cpp @@ -112,6 +112,8 @@ int main(int argc, char** argv) UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT else if(arg=="unreachable-string") UNREACHABLE; + else if(arg == "unreachable-because") + UNREACHABLE_BECAUSE("Unreachable with explanation text"); else if(arg=="data-invariant-structured") DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT else if(arg=="data-invariant-string") diff --git a/regression/invariants/invariant-failure21/test.desc b/regression/invariants/invariant-failure21/test.desc new file mode 100644 index 00000000000..7fe0a52bb5c --- /dev/null +++ b/regression/invariants/invariant-failure21/test.desc @@ -0,0 +1,12 @@ +CORE +dummy_parameter.c +unreachable-because +^EXIT=(0|127|134|137)$ +^SIGNAL=0$ +--- begin invariant violation report --- +Unreachable with explanation text +Invariant check failed +^(Backtrace)|(Backtraces not supported)$ +-- +^warning: ignoring +^VERIFICATION SUCCESSFUL$ diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 0f077101d57..a231850989f 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -516,10 +516,9 @@ constant_exprt smt2_convt::parse_literal( return from_integer(value, type); } else - INVARIANT( - false, + UNREACHABLE_BECAUSE( "smt2_convt::parse_literal should not be of unsupported type " + - type.id_string()); + type.id_string()); } exprt smt2_convt::parse_array( diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp index 2092fca7b2b..c8f07ab666b 100644 --- a/src/solvers/strings/string_format_builtin_function.cpp +++ b/src/solvers/strings/string_format_builtin_function.cpp @@ -232,7 +232,8 @@ add_axioms_for_format_specifier( } } - INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]"); + UNREACHABLE_BECAUSE( + "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]"); } /// Deserialize an argument for format from \p string. diff --git a/src/util/invariant.h b/src/util/invariant.h index cc65115a2ac..620d132e450 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -500,9 +500,33 @@ CBMC_NORETURN void report_invariant_failure( EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) /// This should be used to mark dead code -#define UNREACHABLE INVARIANT(false, "Unreachable") -#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ - EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)) +#ifdef __GNUC__ +// GCC 12 with -O0 fails reporting missing return when using UNREACHABLE. +// Using __builtin_unreachable fixes this without breaking the invariant. +# define UNREACHABLE \ + do \ + { \ + INVARIANT(false, "Unreachable"); \ + __builtin_unreachable(); \ + } while(false) +# define UNREACHABLE_BECAUSE(REASON) \ + do \ + { \ + INVARIANT(false, REASON); \ + __builtin_unreachable(); \ + } while(false) +# define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ + do \ + { \ + EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)); \ + __builtin_unreachable(); \ + } while(false) +#else +# define UNREACHABLE INVARIANT(false, "Unreachable") +# define UNREACHABLE_BECAUSE(REASON) INVARIANT(false, REASON) +# define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ + EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)) +#endif /// This condition should be used to document that assumptions that are /// made on goto_functions, goto_programs, exprts, etc. being well formed. @@ -514,8 +538,17 @@ CBMC_NORETURN void report_invariant_failure( #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) -#define UNIMPLEMENTED_FEATURE(FEATURE) \ - INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE)) +#if __GNUC__ +# define UNIMPLEMENTED_FEATURE(FEATURE) \ + do \ + { \ + INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE)); \ + __builtin_unreachable(); \ + } while(false) +#else +# define UNIMPLEMENTED_FEATURE(FEATURE) \ + INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE)) +#endif // Legacy annotations