Zero vs. non-zero integer value of null pointer constant now configurable

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

Author: kroening

src/util/config.cpp

@@ -248,6 +248,7 @@ void configt::ansi_ct::set_arch_spec_i386()
   arch=ARCH_I386;
   endianness=IS_LITTLE_ENDIAN;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -290,6 +291,7 @@ void configt::ansi_ct::set_arch_spec_x86_64()
   endianness=IS_LITTLE_ENDIAN;
   long_double_width=16*8;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -340,6 +342,7 @@ void configt::ansi_ct::set_arch_spec_power(const irep_idt &subarch)
   endianness=IS_BIG_ENDIAN;
   long_double_width=16*8;
   char_is_unsigned=true;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -392,6 +395,7 @@ void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch)
   arch=ARCH_ARM;
   endianness=IS_LITTLE_ENDIAN;
   char_is_unsigned=true;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -432,6 +436,7 @@ void configt::ansi_ct::set_arch_spec_alpha()
   endianness=IS_LITTLE_ENDIAN;
   long_double_width=16*8;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -473,6 +478,7 @@ void configt::ansi_ct::set_arch_spec_mips(const irep_idt &subarch)
     endianness=IS_BIG_ENDIAN;
   long_double_width=8*8;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -513,6 +519,7 @@ void configt::ansi_ct::set_arch_spec_s390()
   endianness=IS_BIG_ENDIAN;
   long_double_width=16*8;
   char_is_unsigned=true;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -550,6 +557,7 @@ void configt::ansi_ct::set_arch_spec_s390x()
   arch=ARCH_S390X;
   endianness=IS_BIG_ENDIAN;
   char_is_unsigned=true;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -588,6 +596,7 @@ void configt::ansi_ct::set_arch_spec_sparc()
   endianness=IS_BIG_ENDIAN;
   long_double_width=16*8;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -626,6 +635,7 @@ void configt::ansi_ct::set_arch_spec_ia64()
   long_double_width=16*8;
   endianness=IS_LITTLE_ENDIAN;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -667,6 +677,7 @@ void configt::ansi_ct::set_arch_spec_x32()
   arch=ARCH_X32;
   endianness=IS_LITTLE_ENDIAN;
   char_is_unsigned=false;
+  NULL_is_zero=true;
 
   switch(mode)
   {
@@ -713,6 +724,7 @@ bool configt::set(const cmdlinet &cmdline)
   ansi_c.os=ansi_ct::NO_OS;
   ansi_c.arch=ansi_ct::NO_ARCH;
   ansi_c.lib=configt::ansi_ct::LIB_NONE;
+  ansi_c.NULL_is_zero=(size_t)((void*)0)==0;
 
   // Default is ROUND_TO_EVEN, justified by C99:
   // 1 At program startup the floating-point environment is initialized as
@@ -824,6 +836,7 @@ bool configt::set(const cmdlinet &cmdline)
     ansi_c.arch=configt::ansi_ct::NO_ARCH;
     ansi_c.endianness=configt::ansi_ct::NO_ENDIANNESS;
     ansi_c.lib=configt::ansi_ct::LIB_NONE;
+    ansi_c.NULL_is_zero=false;
 
     if(sizeof(long int)==8)
       ansi_c.set_64();

src/util/config.h

@@ -77,6 +77,9 @@ class configt
                    ARCH_IA64, ARCH_X32 } archt;
     archt arch;
 
+    // architecture-specific integer value of null pointer constant
+    bool NULL_is_zero;
+
     void set_arch_spec_i386();
     void set_arch_spec_x86_64();
     void set_arch_spec_power(const irep_idt &subarch);

src/util/simplify_expr.cpp

@@ -316,19 +316,17 @@ 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() &&
      to_constant_expr(expr.op0()).get_value()==ID_NULL &&
-     (expr_type.id()==ID_unsignedbv || expr_type.id()==ID_signedbv))
+     (expr_type.id()==ID_unsignedbv || expr_type.id()==ID_signedbv) &&
+     config.ansi_c.NULL_is_zero)
   {
     exprt tmp=gen_zero(expr_type);
     expr.swap(tmp);
     return false;
   }
-  #endif
 
   // casts from pointer to integer
   // where width of integer >= width of pointer
@@ -790,12 +788,13 @@ static bool is_dereference_integer_object(
 
     if(expr.op0().is_constant())
     {
-      /*if(to_constant_expr(expr.op0()).get_value()==ID_NULL) // NULL
+      if(to_constant_expr(expr.op0()).get_value()==ID_NULL &&
+         config.ansi_c.NULL_is_zero) // NULL
       {
-        address=XXX; // architecture-specific constant
+        address=0;
         return true;
       }
-      else*/ if(!to_integer(expr.op0(), address))
+      else if(!to_integer(expr.op0(), address))
         return true;
     }
   }