Skip to content

Commit d8ba147

Browse files
author
Enrico Steffinlongo
committed
Generated new version of UNIMPLEMENTED_FEATURE addressing error on GCC 12
1 parent 8ea7784 commit d8ba147

File tree

1 file changed

+11
-2
lines changed

1 file changed

+11
-2
lines changed

src/util/invariant.h

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -531,8 +531,17 @@ CBMC_NORETURN void report_invariant_failure(
531531
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
532532
EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
533533

534-
#define UNIMPLEMENTED_FEATURE(FEATURE) \
535-
INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
534+
#if __GNUC__
535+
# define UNIMPLEMENTED_FEATURE(FEATURE) \
536+
do \
537+
{ \
538+
INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE)); \
539+
__builtin_unreachable(); \
540+
} while(false)
541+
#else
542+
# define UNIMPLEMENTED_FEATURE(FEATURE) \
543+
INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
544+
#endif
536545

537546
// Legacy annotations
538547

0 commit comments

Comments
 (0)