Pointer subtraction in back-end: no need for bounds checking

5b8028a added pointer validity checks in the back-end when
performing pointer minus pointer operations. Given our pointer encoding
it seems important to do a same-object test as, for distinct objects,
the object identifier part would start to play into the subtraction.
When operating on the same object, however, even out-of-bounds pointers'
subtraction should be indistinguishable from how this works on actual
hardware.

Therefore, this commit removes the bounds-checking part. (C semantics
have a pointer-validity requirement, but we need to catch this via
checks inserted in the front-end, not in the back-end.)

Author: tautschnig

src/solvers/flattening/bv_pointers.cpp

@@ -665,39 +665,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
           difference, element_size_bv, bv_utilst::representationt::SIGNED);
       }
 
-      // test for null object (integer constants)
-      const exprt null_object = ::null_object(minus_expr.lhs());
-      literalt in_bounds = convert(null_object);
-
-      if(!in_bounds.is_true())
-      {
-        // compute the object size (again, possibly using cached results)
-        const exprt object_size = ::object_size(minus_expr.lhs());
-        const bvt object_size_bv =
-          bv_utils.zero_extension(convert_bv(object_size), width);
-
-        const literalt lhs_in_bounds = prop.land(
-          !bv_utils.sign_bit(lhs_offset),
-          bv_utils.rel(
-            lhs_offset,
-            ID_le,
-            object_size_bv,
-            bv_utilst::representationt::UNSIGNED));
-
-        const literalt rhs_in_bounds = prop.land(
-          !bv_utils.sign_bit(rhs_offset),
-          bv_utils.rel(
-            rhs_offset,
-            ID_le,
-            object_size_bv,
-            bv_utilst::representationt::UNSIGNED));
-
-        in_bounds =
-          prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
-      }
-
-      prop.l_set_to_true(prop.limplies(
-        prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
+      prop.l_set_to_true(
+        prop.limplies(same_object_lit, bv_utils.equal(difference, bv)));
     }
 
     return bv;