Properly distinguish null pointer constants and (T*)0

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

Author: kroening

src/ansi-c/expr2c.cpp

@@ -579,11 +579,6 @@ std::string expr2ct::convert_typecast(
      from_type.id()==ID_unsignedbv)
     return convert(src.op(), precedence);
 
-  if(to_type.id()==ID_pointer &&
-     ns.follow(to_type.subtype()).id()==ID_empty && // to (void *)?
-     src.op0().is_zero())
-    return "NULL";
-
   std::string dest="("+convert(to_type)+")";
 
   unsigned p;
@@ -2079,7 +2074,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_pointer)
   {
-    if(src.is_zero())
+    if(to_constant_expr(src).get_value()==ID_NULL)
     {
       dest="NULL";
       if(type.subtype().id()!=ID_empty)

src/solvers/flattening/bv_pointers.cpp

@@ -307,7 +307,6 @@ void bv_pointerst::convert_pointer_type(const exprt &expr, bvt &bv)
             op_type.id()==ID_c_enum)
     {
       // Cast from integer to pointer.
-      // We need to be able to convert the integer 0 to NULL.
       // We just do a zero extension.
 
       const bvt &op_bv=convert_bv(op);

src/util/expr.cpp

@@ -477,7 +477,6 @@ bool exprt::is_zero() const
     }
     else if(type_id==ID_pointer)
     {
-      if(constant.get_value()==ID_NULL) return true;
       return constant.value_is_zero_string();
     }
   }

src/util/simplify_expr.cpp

@@ -316,6 +316,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     return false;
   }
 
+  #if 0
+  // should be architecture-specific constant
   // casts from NULL to any integer
   if(op_type.id()==ID_pointer &&
      expr.op0().is_constant() &&
@@ -326,6 +328,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     expr.swap(tmp);
     return false;
   }
+  #endif
 
   // casts from pointer to integer
   // where width of integer >= width of pointer
@@ -785,10 +788,15 @@ static bool is_dereference_integer_object(
        !to_integer(expr.op0().op0(), address))
       return true;
 
-    if(expr.op0().is_zero()) // NULL
+    if(expr.op0().is_constant())
     {
-      address=0;
-      return true;
+      /*if(to_constant_expr(expr.op0()).get_value()==ID_NULL) // NULL
+      {
+        address=XXX; // architecture-specific constant
+        return true;
+      }
+      else*/ if(!to_integer(expr.op0(), address))
+        return true;
     }
   }
 
@@ -3520,7 +3528,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
         // note that 'ptr' may be an integer
         exprt op=expr.op0().op0();
         expr.op0().swap(op);
-        expr.op1()=gen_zero(expr.op0().type());
+        expr.op1().type()=expr.op0().type();
         simplify_inequality(expr); // do again!
         return false;
       }