Mimic GCC/Clang simplification behaviour when type checking ?:

Neither GCC nor Clang simplify expressions involving symbols even when
the result would always be 0, which our simplifier figure out.

Fixes: #7927

Author: tautschnig

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/sizeof6/test.desc

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

src/ansi-c/c_typecheck_expr.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/find_symbols.h>
 #include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
@@ -1608,17 +1609,20 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
     exprt tmp1=simplify_expr(operands[1], *this);
     exprt tmp2=simplify_expr(operands[2], *this);
 
-    // is one of them void * AND null? Convert that to the other.
-    // (at least that's how GCC behaves)
+    // Is one of them void * AND null? Convert that to the other.
+    // (At least that's how GCC, Clang, and Visual Studio behave. Presence of
+    // symbols blocks them from simplifying the expression to NULL.)
     if(
       to_pointer_type(operands[1].type()).base_type().id() == ID_empty &&
-      tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1)))
+      tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1)) &&
+      find_symbols(operands[1]).empty())
     {
       implicit_typecast(operands[1], operands[2].type());
     }
     else if(
       to_pointer_type(operands[2].type()).base_type().id() == ID_empty &&
-      tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2)))
+      tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2)) &&
+      find_symbols(operands[2]).empty())
     {
       implicit_typecast(operands[2], operands[1].type());
     }