Rename ID_invalid_pointer to ID_is_invalid_pointer

This is a more accurate name

Author: Owen

src/analyses/goto_check.cpp

@@ -1129,18 +1129,18 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
     if(flags.is_unknown())
     {
-      conditions.push_back(conditiont(
-        not_exprt(invalid_pointer(address)),
-        "pointer invalid"));
+      conditions.push_back(
+        conditiont(not_exprt(is_invalid_pointer(address)), "pointer invalid"));
     }
 
     if(flags.is_uninitialized())
     {
-      conditions.push_back(conditiont(
-        or_exprt(
-          in_bounds_of_some_explicit_allocation,
-          not_exprt(invalid_pointer(address))),
-        "pointer uninitialized"));
+      conditions.push_back(
+        conditiont(
+          or_exprt(
+            in_bounds_of_some_explicit_allocation,
+            not_exprt(is_invalid_pointer(address))),
+          "pointer uninitialized"));
     }
 
     if(flags.is_unknown() || flags.is_dynamic_heap())

src/ansi-c/c_typecheck_expr.cpp

@@ -2095,16 +2095,16 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(get_may_expr);
   }
-  else if(identifier==CPROVER_PREFIX "invalid_pointer")
+  else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
   {
     if(expr.arguments().size()!=1)
     {
       error().source_location = f_op.source_location();
-      error() << "invalid_pointer expects one operand" << eom;
+      error() << "is_invalid_pointer expects one operand" << eom;
       throw 0;
     }
 
-    exprt same_object_expr = invalid_pointer(expr.arguments().front());
+    exprt same_object_expr = is_invalid_pointer(expr.arguments().front());
     same_object_expr.add_source_location()=source_location;
 
     return same_object_expr;

src/ansi-c/cprover_builtin_headers.h

@@ -5,7 +5,7 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description
 void __CPROVER_havoc_object(void *);
 __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
-__CPROVER_bool __CPROVER_invalid_pointer(const void *);
+__CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);

src/ansi-c/expr2c.cpp

@@ -3426,8 +3426,8 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id() == ID_w_ok)
     return convert_function(src, "W_OK", precedence = 16);
 
-  else if(src.id()==ID_invalid_pointer)
-    return convert_function(src, "INVALID-POINTER", precedence=16);
+  else if(src.id() == ID_is_invalid_pointer)
+    return convert_function(src, "IS-INVALID-POINTER", precedence = 16);
 
   else if(src.id()==ID_good_pointer)
     return convert_function(src, "GOOD_POINTER", precedence=16);
@@ -3482,9 +3482,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()=="pointer_cons")
     return convert_function(src, "POINTER_CONS", precedence=16);
 
-  else if(src.id()==ID_invalid_pointer)
+  else if(src.id() == ID_is_invalid_pointer)
     return convert_function(
-      src, CPROVER_PREFIX "invalid_pointer", precedence = 16);
+      src, CPROVER_PREFIX "is_invalid_pointer", precedence = 16);
 
   else if(src.id() == ID_is_dynamic_object)
     return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16);

src/solvers/flattening/bv_pointers.cpp

@@ -20,7 +20,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
 
   const exprt::operandst &operands=expr.operands();
 
-  if(expr.id()==ID_invalid_pointer)
+  if(expr.id() == ID_is_invalid_pointer)
   {
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)

src/solvers/smt2/smt2_conv.cpp

@@ -1320,7 +1320,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     convert_is_dynamic_object(expr);
   }
-  else if(expr.id()==ID_invalid_pointer)
+  else if(expr.id() == ID_is_invalid_pointer)
   {
     DATA_INVARIANT(
       expr.operands().size() == 1,

src/util/irep_ids.def

@@ -217,7 +217,7 @@ IREP_ID_ONE(invalid)
 IREP_ID_TWO(C_invalid_object, #invalid_object)
 IREP_ID_ONE(pointer_offset)
 IREP_ID_ONE(pointer_object)
-IREP_ID_TWO(invalid_pointer, invalid-pointer)
+IREP_ID_TWO(is_invalid_pointer, is-invalid-pointer)
 IREP_ID_ONE(ieee_float_equal)
 IREP_ID_ONE(ieee_float_notequal)
 IREP_ID_ONE(isnan)

src/util/pointer_predicates.cpp

@@ -105,7 +105,7 @@ exprt good_pointer_def(
 
   const not_exprt not_null(null_pointer(pointer));
 
-  const not_exprt not_invalid(invalid_pointer(pointer));
+  const not_exprt not_invalid(is_invalid_pointer(pointer));
 
   const or_exprt bad_other(
     object_lower_bound(pointer, nil_exprt()),
@@ -139,9 +139,9 @@ exprt null_pointer(const exprt &pointer)
   return same_object(pointer, null_pointer);
 }
 
-exprt invalid_pointer(const exprt &pointer)
+exprt is_invalid_pointer(const exprt &pointer)
 {
-  return unary_exprt(ID_invalid_pointer, pointer, bool_typet());
+  return unary_exprt(ID_is_invalid_pointer, pointer, bool_typet());
 }
 
 exprt dynamic_object_lower_bound(

src/util/pointer_predicates.h

@@ -32,7 +32,7 @@ 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 invalid_pointer(const exprt &pointer);
+exprt is_invalid_pointer(const exprt &pointer);
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
   const exprt &offset);

src/util/simplify_expr.cpp

@@ -2407,8 +2407,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
   {
     result = simplify_is_dynamic_object(expr) && result;
   }
-  else if(expr.id()==ID_invalid_pointer)
-    result=simplify_invalid_pointer(expr) && result;
+  else if(expr.id() == ID_is_invalid_pointer)
+    result = simplify_is_invalid_pointer(expr) && result;
   else if(expr.id()==ID_object_size)
     result=simplify_object_size(expr) && result;
   else if(expr.id()==ID_good_pointer)

src/util/simplify_expr_class.h

@@ -97,7 +97,7 @@ class simplify_exprt
   bool simplify_object_size(exprt &expr);
   bool simplify_dynamic_size(exprt &expr);
   bool simplify_is_dynamic_object(exprt &expr);
-  bool simplify_invalid_pointer(exprt &expr);
+  bool simplify_is_invalid_pointer(exprt &expr);
   bool simplify_same_object(exprt &expr);
   bool simplify_good_pointer(exprt &expr);
   bool simplify_object(exprt &expr);

src/util/simplify_expr_pointer.cpp

@@ -571,7 +571,7 @@ bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
   return result;
 }
 
-bool simplify_exprt::simplify_invalid_pointer(exprt &expr)
+bool simplify_exprt::simplify_is_invalid_pointer(exprt &expr)
 {
   if(expr.operands().size()!=1)
     return true;