Any compile-time integer constant expression evaluating

 to 0 is a null pointer constant

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

Author: kroening

regression/cbmc/null1/main.c

@@ -0,0 +1,10 @@
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1];
+
+STATIC_ASSERT((void*)0==(void*)(1-1));
+
+int main()
+{
+  assert((void*)0==(void*)('a'-'a'));
+  return 0;
+}

regression/cbmc/null1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--all-claims --no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.1\] assertion NULL == NULL: OK$
+^\*\* 0 of 1 failed (1 iterations)$
+--
+^warning: ignoring

src/ansi-c/c_typecast.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/base_type.h>
 #include <util/symbol.h>
+#include <util/simplify_expr.h>
 
 #include "c_typecast.h"
 #include "c_types.h"
@@ -549,7 +550,7 @@ void c_typecastt::implicit_typecast_followed(
   {
     // special case: 0 == NULL
 
-    if(expr.is_zero() && (
+    if(simplify_expr(expr, ns).is_zero() && (
        src_type.id()==ID_unsignedbv ||
        src_type.id()==ID_signedbv ||
        src_type.id()==ID_natural ||

src/ansi-c/c_typecheck_expr.cpp

@@ -1179,7 +1179,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
 
   // special case: NULL
   if(expr_type.id()==ID_pointer &&
-     op.is_zero())
+     simplify_expr(op, *this).is_zero())
   {
     // zero typecasted to a pointer is NULL
     constant_exprt result(ID_NULL, expr_type);
@@ -1400,31 +1400,18 @@ void c_typecheck_baset::typecheck_expr_rel(exprt &expr)
   }
   else
   {
-    // pointer and zero
-    if(type0.id()==ID_pointer && op1.is_zero())
-    {
-      op1=constant_exprt(type0);
-      op1.set(ID_value, ID_NULL);
-      return;
-    }
-
-    if(type1.id()==ID_pointer && op0.is_zero())
-    {
-      op0=constant_exprt(type1);
-      op0.set(ID_value, ID_NULL);
-      return;
-    }
-
     // pointer and integer
     if(type0.id()==ID_pointer && is_number(type1))
     {
       op1.make_typecast(type0);
+      typecheck_expr_typecast(op1);
       return;
     }
 
     if(type1.id()==ID_pointer && is_number(type0))
     {
       op0.make_typecast(type1);
+      typecheck_expr_typecast(op0);
       return;
     }
 

src/cpp/cpp_typecheck_conversions.cpp

@@ -13,6 +13,7 @@ Module: C++ Language Type Checking
 #include <util/expr_util.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
+#include <util/simplify_expr.h>
 
 #include <ansi-c/c_qualifiers.h>
 #include <ansi-c/c_types.h>
@@ -560,7 +561,7 @@ bool cpp_typecheckt::standard_conversion_pointer(
     return false;
 
   // integer 0 to NULL pointer conversion?
-  if(expr.is_zero() &&
+  if(simplify_expr(expr, *this).is_zero() &&
      expr.type().id()!=ID_pointer)
   {
     new_expr = expr;
@@ -2088,7 +2089,7 @@ bool cpp_typecheckt::reinterpret_typecast(
      && !is_reference(type))
   {
     // integer to pointer
-    if(e.is_zero())
+    if(simplify_expr(e, *this).is_zero())
     {
       // NULL
       new_expr = e;