Fixed UNREACHABLE missing return warning on GCC 12

GCC 12 wshen using `-O0` fails because of a missing-return-statement
warning caused by the implementation of `INVARIANT(false)`.
This is beacause the condition `if (true)` is not considered exaustive.
The solution involves marking the unreachable path as
`__builtin_unreachable()`.

Author: Enrico Steffinlongo

src/util/invariant.h

@@ -500,9 +500,26 @@ 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_STRUCTURED(TYPENAME, ...)                                \
+    do                                                                         \
+    {                                                                          \
+      EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__));        \
+      __builtin_unreachable();                                                 \
+    } while(false)
+#else
+#  define UNREACHABLE INVARIANT(false, "Unreachable")
+#  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.