Mimic GCC/Clang simplification behaviour when type checking ?:

regression/ansi-c/sizeof6/main.c

@@ -0,0 +1,23 @@
+int main()
+{
+  long long i;
+#ifndef _MSC_VER
+  _Static_assert(sizeof(int) == sizeof(*(1 ? ((void *)(0ll)) : (int *)1)), "");
+  // We are able to simplify all of the expressions involving i below to 0, but
+  // GCC and Clang don't do so. Hence, the static asserts pass for those
+  // compilers.
+  _Static_assert(
+    sizeof(int) != sizeof(*(1 ? ((void *)(i * 0)) : (int *)1)), "");
+  _Static_assert(
+    sizeof(int) != sizeof(*(1 ? ((void *)(i - i)) : (int *)1)), "");
+  _Static_assert(
+    sizeof(int) != sizeof(*(1 ? ((void *)(i ? 0ll : 0ll)) : (int *)1)), "");
+  _Static_assert(
+    sizeof(int) != sizeof(*(1 ? ((void *)(0 ? i : 0ll)) : (int *)1)), "");
+#else
+  static_assert(sizeof(int) == sizeof(*(1 ? ((void *)(0)) : (int *)1)), "");
+  // Visual Studio rejects this as "illegal indirection"
+  // static_assert(
+  //   sizeof(int) == sizeof(*(1 ? ((void *)(i * 0)) : (int *)1)), "");
+#endif
+}

regression/ansi-c/gcc_builtin_constant_p1/test.desc → regression/ansi-c/sizeof6/test.desc

@@ -1,4 +1,4 @@
-CORE gcc-only broken-test-c++-front-end
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/gcc_builtin_constant_p1/main.c

@@ -0,0 +1,47 @@
+#include <assert.h>
+
+#ifdef __GNUC__
+enum
+{
+  E1 = 1
+} var;
+
+struct whatnot
+{
+} whatnot_var;
+#endif
+
+int main()
+{
+  // this is gcc only
+
+#ifdef __GNUC__
+  assert(__builtin_constant_p("some string"));
+  assert(__builtin_constant_p(1.0f));
+  assert(__builtin_constant_p(E1));
+  assert(!__builtin_constant_p(var));
+  assert(!__builtin_constant_p(main));
+  assert(!__builtin_constant_p(whatnot_var));
+  assert(!__builtin_constant_p(&var));
+  assert(__builtin_constant_p(__builtin_constant_p(var)));
+
+  // The following are not constant expressions in the sense of the C standard
+  // and GCC wouldn't deem them constant expressions either, but they are
+  // subject to GCC's constant folding. See also regression test ansi-c/sizeof6.
+  // Clang's behaviour, however, is somewhat different. See
+  // https://github.com/llvm/llvm-project/issues/55946 for further examples of
+  // where they differ.
+  int j;
+#  ifndef __clang__
+  assert(__builtin_constant_p(j * 0));
+  assert(__builtin_constant_p(j - j));
+  assert(__builtin_constant_p(j ? 0ll : 0ll));
+#  endif
+  assert(__builtin_constant_p(0 ? j : 0ll));
+
+  // side-effects are _not_ evaluated
+  int i = 0;
+  assert(!__builtin_constant_p(i++));
+  assert(i == 0);
+#endif
+}

regression/cbmc/gcc_builtin_constant_p1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$