Remove unnecessary use of ns.follow from pointer predicates

This also makes the namespace unnecessary in three cases.

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1173,7 +1173,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
       const or_exprt dynamic_bounds_violation(
-        dynamic_object_lower_bound(address, ns, nil_exprt()),
+        dynamic_object_lower_bound(address, nil_exprt()),
         dynamic_object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
@@ -1189,8 +1189,8 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
       flags.is_static_lifetime())
     {
       const or_exprt object_bounds_violation(
-        object_lower_bound(address, ns, nil_exprt()),
-        object_upper_bound(address, ns, size));
+        object_lower_bound(address, nil_exprt()),
+        object_upper_bound(address, size));
 
       conditions.push_back(conditiont(
         or_exprt(

src/util/pointer_predicates.cpp

@@ -84,16 +84,15 @@ exprt good_pointer_def(
   const exprt &pointer,
   const namespacet &ns)
 {
-  const pointer_typet &pointer_type=to_pointer_type(ns.follow(pointer.type()));
+  const pointer_typet &pointer_type = to_pointer_type(pointer.type());
   const typet &dereference_type=pointer_type.subtype();
 
   const or_exprt good_dynamic_tmp1(
     not_exprt(malloc_object(pointer, ns)),
     and_exprt(
-      not_exprt(dynamic_object_lower_bound(pointer, ns, nil_exprt())),
-      not_exprt(
-        dynamic_object_upper_bound(
-          pointer, ns, size_of_expr(dereference_type, ns)))));
+      not_exprt(dynamic_object_lower_bound(pointer, nil_exprt())),
+      not_exprt(dynamic_object_upper_bound(
+        pointer, ns, size_of_expr(dereference_type, ns)))));
 
   const and_exprt good_dynamic_tmp2(
     not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
@@ -106,9 +105,8 @@ exprt good_pointer_def(
   const not_exprt not_invalid(invalid_pointer(pointer));
 
   const or_exprt bad_other(
-    object_lower_bound(pointer, ns, nil_exprt()),
-    object_upper_bound(
-      pointer, ns, size_of_expr(dereference_type, ns)));
+    object_lower_bound(pointer, nil_exprt()),
+    object_upper_bound(pointer, size_of_expr(dereference_type, ns)));
 
   const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
 
@@ -145,10 +143,9 @@ exprt invalid_pointer(const exprt &pointer)
 
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &offset)
 {
-  return object_lower_bound(pointer, ns, offset);
+  return object_lower_bound(pointer, offset);
 }
 
 exprt dynamic_object_upper_bound(
@@ -171,22 +168,17 @@ exprt dynamic_object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, access_size.type()),
+      access_size);
   }
 
-  if(ns.follow(sum.type())!=
-     ns.follow(malloc_size.type()))
-    sum.make_typecast(malloc_size.type());
-
-  return binary_relation_exprt(sum, op, malloc_size);
+  return binary_relation_exprt(
+    typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
 }
 
 exprt object_upper_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &access_size)
 {
   // this is
@@ -204,23 +196,19 @@ exprt object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, access_size.type()),
+      access_size);
   }
 
-
-  if(ns.follow(sum.type())!=
-     ns.follow(object_size_expr.type()))
-    sum.make_typecast(object_size_expr.type());
-
-  return binary_relation_exprt(sum, op, object_size_expr);
+  return binary_relation_exprt(
+    typecast_exprt::conditional_cast(sum, object_size_expr.type()),
+    op,
+    object_size_expr);
 }
 
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &offset)
 {
   exprt p_offset=pointer_offset(pointer);
@@ -230,11 +218,8 @@ exprt object_lower_bound(
 
   if(offset.is_not_nil())
   {
-    if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
-      p_offset=
-        plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
-    else
-      p_offset=plus_exprt(p_offset, offset);
+    p_offset = plus_exprt(
+      p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
   }
 
   return binary_relation_exprt(p_offset, ID_lt, zero);

src/util/pointer_predicates.h

@@ -33,19 +33,16 @@ exprt integer_address(const exprt &pointer);
 exprt invalid_pointer(const exprt &pointer);
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &offset);
 exprt dynamic_object_upper_bound(
   const exprt &pointer,
   const namespacet &,
   const exprt &access_size);
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &offset);
 exprt object_upper_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &access_size);
 
 #endif // CPROVER_UTIL_POINTER_PREDICATES_H