Merge pull request #5689 from tautschnig/pointer-simpl

Simplification of pointer comparison: do not assume numeric types

Author: tautschnig

regression/cbmc-library/memcpy-06/main.c

@@ -0,0 +1,16 @@
+// #include <string.h> is intentionally missing
+
+struct c
+{
+};
+
+int d()
+{
+  struct c e;
+  memcpy(e);
+}
+int main()
+{
+  int (*h)() = d;
+  h();
+}

regression/cbmc-library/memcpy-06/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+function 'memcpy' is not declared
+parameter "memcpy::dst" type mismatch
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed

src/util/simplify_expr_int.cpp

@@ -1645,14 +1645,19 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
         }
       }
       else if(
-        expr.op0().id() == ID_typecast &&
-        expr.op0().type().id() == ID_pointer &&
-        (to_typecast_expr(expr.op0()).op().type().id() == ID_pointer ||
-         config.ansi_c.NULL_is_zero))
+        expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_pointer)
       {
+        exprt op = to_typecast_expr(expr.op0()).op();
+        if(
+          op.type().id() != ID_pointer &&
+          (!config.ansi_c.NULL_is_zero || !is_number(op.type()) ||
+           op.type().id() == ID_complex))
+        {
+          return unchanged(expr);
+        }
+
         // (type)ptr == NULL -> ptr == NULL
         // note that 'ptr' may be an integer
-        exprt op = to_typecast_expr(expr.op0()).op();
         auto new_expr = expr;
         new_expr.op0().swap(op);
         if(new_expr.op0().type().id() != ID_pointer)