Use null_pointer_exprt instead of gen_zero

Author: tautschnig

src/analyses/goto_check.cpp

@@ -972,7 +972,8 @@ void goto_checkt::pointer_validity_check(
     return;
 
   const exprt &pointer=expr.op0();
-  const typet &pointer_type=to_pointer_type(ns.follow(pointer.type()));
+  const pointer_typet &pointer_type=
+    to_pointer_type(ns.follow(pointer.type()));
 
   assert(base_type_eq(pointer_type.subtype(), expr.type(), ns));
 
@@ -986,7 +987,7 @@ void goto_checkt::pointer_validity_check(
   {
     if(flags.is_unknown() || flags.is_null())
     {
-      notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
+      notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type));
 
       add_guarded_claim(
         not_eq_null,
@@ -1612,7 +1613,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
 
         if(flags.is_unknown() || flags.is_null())
         {
-          notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
+          notequal_exprt not_eq_null(
+            pointer,
+            null_pointer_exprt(to_pointer_type(pointer.type())));
 
           add_guarded_claim(
             not_eq_null,
@@ -1651,7 +1654,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
 
         if(pointer.type().subtype().get(ID_identifier)!="java::java.lang.AssertionError")
         {
-          notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
+          notequal_exprt not_eq_null(
+            pointer,
+            null_pointer_exprt(to_pointer_type(pointer.type())));
 
           add_guarded_claim(
             not_eq_null,
@@ -1718,7 +1723,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
         source_locationt source_location;
         source_location.set_function(i.function);
 
-        equal_exprt eq(leak_expr, gen_zero(ns.follow(leak.type)));
+        equal_exprt eq(
+          leak_expr,
+          null_pointer_exprt(to_pointer_type(leak.type)));
         add_guarded_claim(
           eq,
           "dynamically allocated memory never freed",

src/cpp/cpp_typecheck_virtual_table.cpp

@@ -47,8 +47,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
     if(compo.get_bool("is_pure_virtual"))
     {
       pointer_typet pointer_type(code_type);
-      e = gen_zero(pointer_type);
-      assert(e.is_not_nil());
+      e=null_pointer_exprt(pointer_type);
       value_map[compo.get("virtual_name")] = e;
     }
     else

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -906,7 +906,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     if(statement=="aconst_null")
     {
       assert(results.size()==1);
-      results[0]=gen_zero(java_reference_type(void_typet()));
+      results[0]=null_pointer_exprt(java_reference_type(void_typet()));
     }
     else if(statement=="athrow")
     {
@@ -1370,7 +1370,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(op.size()==1 && results.empty());
       code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
-      const exprt rhs(gen_zero(lhs.type()));
+      const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
       code_branch.then_case()=code_gotot(label(number));
       code_branch.then_case().add_source_location()=i_it->source_location;
@@ -1384,7 +1384,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       irep_idt number=to_constant_expr(arg0).get_value();
       code_ifthenelset code_branch;
       const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
-      const exprt rhs(gen_zero(lhs.type()));
+      const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
       code_branch.then_case()=code_gotot(label(number));
       code_branch.then_case().add_source_location()=i_it->source_location;

src/java_bytecode/java_types.cpp

@@ -183,7 +183,7 @@ Function: java_reference_type
 
 \*******************************************************************/
 
-typet java_reference_type(const typet &subtype)
+reference_typet java_reference_type(const typet &subtype)
 {
   return reference_typet(subtype);
 }

src/java_bytecode/java_types.h

@@ -20,7 +20,7 @@ typet java_char_type();
 typet java_float_type();
 typet java_double_type();
 typet java_boolean_type();
-typet java_reference_type(const typet &subtype);
+reference_typet java_reference_type(const typet &subtype);
 symbol_typet java_classname(const std::string &);
 
 pointer_typet java_array_type(const char subtype);

src/util/arith_tools.cpp

@@ -188,11 +188,7 @@ constant_exprt from_integer(
   else if(type_id==ID_pointer)
   {
     if(int_value==0)
-    {
-      constant_exprt result(type);
-      result.set_value(ID_NULL);
-      return result;
-    }
+      return null_pointer_exprt(to_pointer_type(type));
   }
   else if(type_id==ID_c_bit_field)
   {

src/util/simplify_expr.cpp

@@ -543,8 +543,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
               operand.is_false() &&
               config.ansi_c.NULL_is_zero)
       {
-        expr=gen_zero(expr_type);
-        assert(expr.is_not_nil());
+        expr=null_pointer_exprt(to_pointer_type(expr_type));
         return false;
       }
     }