Pointer subtraction requires same-object and valid-pointer property

Subtracting pointers not pointing into the same (array) object (or one
byte past the object) is undefined behaviour.

Author: tautschnig

regression/cbmc-library/posix_memalign-02/test.desc

@@ -6,6 +6,5 @@ main.c
 ^VERIFICATION FAILED$
 \[main.precondition_instance.1\] .* memcpy src/dst overlap: FAILURE
 \[main.precondition_instance.3\] .* memcpy destination region writeable: FAILURE
-\*\* 2 of 14 failed
 --
 ^warning: ignoring

regression/cbmc/Pointer_difference2/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int array[2];
+  int other_array[2];
+
+  int diff = array - other_array;
+
+  return 0;
+}

regression/cbmc/Pointer_difference2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^\[main.pointer.1\] line 6 same object violation in array - other_array: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/analyses/goto_check.cpp

@@ -178,7 +178,7 @@ class goto_checkt
   void mod_overflow_check(const mod_exprt &, const guardt &);
   void enum_range_check(const exprt &, const guardt &);
   void undefined_shift_check(const shift_exprt &, const guardt &);
-  void pointer_rel_check(const binary_relation_exprt &, const guardt &);
+  void pointer_rel_check(const binary_exprt &, const guardt &);
   void pointer_overflow_check(const exprt &, const guardt &);
 
   /// Generates VCCs for the validity of the given dereferencing operation.
@@ -1117,7 +1117,7 @@ void goto_checkt::nan_check(
 }
 
 void goto_checkt::pointer_rel_check(
-  const binary_relation_exprt &expr,
+  const binary_exprt &expr,
   const guardt &guard)
 {
   if(!enable_pointer_check)
@@ -1137,6 +1137,25 @@ void goto_checkt::pointer_rel_check(
       expr.find_source_location(),
       expr,
       guard);
+
+    for(const auto &pointer : expr.operands())
+    {
+      // just this particular byte must be within object bounds or one past the
+      // end
+      const auto size = from_integer(0, size_type());
+      auto conditions = get_pointer_dereferenceable_conditions(pointer, size);
+
+      for(const auto &c : conditions)
+      {
+        add_guarded_property(
+          c.assertion,
+          "pointer relation: " + c.description,
+          "pointer arithmetic",
+          expr.find_source_location(),
+          pointer,
+          guard);
+      }
+    }
   }
 }
 
@@ -1647,6 +1666,14 @@ void goto_checkt::check_rec_arithmetic_op(const exprt &expr, guardt &guard)
   if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
   {
     integer_overflow_check(expr, guard);
+
+    if(
+      expr.operands().size() == 2 && expr.id() == ID_minus &&
+      expr.operands()[0].type().id() == ID_pointer &&
+      expr.operands()[1].type().id() == ID_pointer)
+    {
+      pointer_rel_check(to_binary_expr(expr), guard);
+    }
   }
   else if(expr.type().id() == ID_floatbv)
   {