Merge pull request #7385 from tautschnig/cleanup/null_pointer_predicate

Remove null_pointer predicate

Author: kroening

src/ansi-c/goto_check_c.cpp

@@ -2405,7 +2405,7 @@ goto_check_ct::get_pointer_is_null_condition(
     return {conditiont{
       or_exprt{
         is_in_bounds_of_some_explicit_allocation(address, size),
-        not_exprt(null_pointer(address))},
+        not_exprt(null_object(address))},
       "pointer NULL"}};
   }
 

src/cprover/axioms.cpp

@@ -474,8 +474,8 @@ void axiomst::node(const exprt &src)
 
     {
       // live_object(ς, p) --> p!=0
-      auto instance = replace(implies_exprt(
-        src, not_exprt(null_pointer(live_object_expr.address()))));
+      auto instance = replace(
+        implies_exprt(src, not_exprt(null_object(live_object_expr.address()))));
       if(verbose)
         std::cout << "AXIOMc: " << format(instance) << "\n";
       dest << instance;
@@ -691,7 +691,7 @@ void axiomst::add(const state_ok_exprt &ok_expr)
   {
     // X_ok(ς, p) --> p!=0
     auto instance =
-      replace(implies_exprt(ok_expr, not_exprt(null_pointer(pointer))));
+      replace(implies_exprt(ok_expr, not_exprt(null_object(pointer))));
     if(verbose)
       std::cout << "AXIOMe: " << format(instance) << "\n";
     dest << instance;

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -607,8 +607,8 @@ void instrument_spec_assignst::create_snapshot(
   dest.add(goto_programt::make_assignment(
     car.valid_var(),
     simplify_expr(
-      and_exprt{car.condition(),
-                not_exprt{null_pointer(car.target_start_address())}},
+      and_exprt{
+        car.condition(), not_exprt{null_object(car.target_start_address())}},
       ns),
     source_location));
 
@@ -640,7 +640,7 @@ exprt instrument_spec_assignst::target_validity_expr(
              w_ok_exprt{car.target_start_address(), car.target_size()}};
 
   if(allow_null_target)
-    result.add_to_operands(null_pointer(car.target_start_address()));
+    result.add_to_operands(null_object(car.target_start_address()));
 
   return simplify_expr(result, ns);
 }
@@ -748,7 +748,7 @@ exprt instrument_spec_assignst::inclusion_check_full(
     // we reach this program point, otherwise we should never reach
     // this program point
     if(allow_null_lhs)
-      return null_pointer(car.target_start_address());
+      return null_object(car.target_start_address());
     else
       return false_exprt{};
   }
@@ -798,7 +798,7 @@ exprt instrument_spec_assignst::inclusion_check_full(
 
   if(allow_null_lhs)
     return or_exprt{
-      null_pointer(car.target_start_address()),
+      null_object(car.target_start_address()),
       and_exprt{car.valid_var(), disjunction(disjuncts)}};
   else
     return and_exprt{car.valid_var(), disjunction(disjuncts)};

src/util/pointer_predicates.cpp

@@ -73,7 +73,7 @@ exprt good_pointer_def(
 
   const exprt good_dynamic = not_exprt{deallocated(pointer, ns)};
 
-  const not_exprt not_null(null_pointer(pointer));
+  const not_exprt not_null(null_object(pointer));
 
   const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
 
@@ -97,12 +97,6 @@ exprt integer_address(const exprt &pointer)
                    notequal_exprt(null_pointer, pointer));
 }
 
-exprt null_pointer(const exprt &pointer)
-{
-  null_pointer_exprt null_pointer(to_pointer_type(pointer.type()));
-  return same_object(pointer, null_pointer);
-}
-
 exprt object_upper_bound(
   const exprt &pointer,
   const exprt &access_size)

src/util/pointer_predicates.h

@@ -25,7 +25,7 @@ exprt object_size(const exprt &pointer);
 exprt good_pointer(const exprt &pointer);
 exprt good_pointer_def(const exprt &pointer, const namespacet &);
 exprt null_object(const exprt &pointer);
-exprt null_pointer(const exprt &pointer);
+
 exprt integer_address(const exprt &pointer);
 exprt object_lower_bound(
   const exprt &pointer,