Turn NULL into constant of proper type when removing

typecasts

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4715 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/null2/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  long tmp;
+  if((void*)tmp)
+  {
+    tmp=1;
+  }
+  assert(tmp!=0);
+
+  return 0;
+}

regression/cbmc/null2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^wrong value length in constant

src/util/simplify_expr.cpp

@@ -3643,13 +3643,18 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       }
       else if(expr.op0().id()==ID_typecast &&
               expr.op0().operands().size()==1 &&
-              expr.op0().type().id()==ID_pointer)
+              expr.op0().type().id()==ID_pointer &&
+              (expr.op0().op0().type().id()==ID_pointer ||
+               config.ansi_c.NULL_is_zero))
       {
         // (type)ptr == NULL -> ptr == NULL
         // note that 'ptr' may be an integer
         exprt op=expr.op0().op0();
         expr.op0().swap(op);
-        expr.op1().type()=expr.op0().type();
+        if(expr.op0().type().id()!=ID_pointer)
+          expr.op1()=gen_zero(expr.op0().type());
+        else
+          expr.op1().type()=expr.op0().type();
         simplify_inequality(expr); // do again!
         return false;
       }