Pointer arithmetic check: do not use pointer-to-int conversion

We do not currently have a sound pointer-to-int conversion, and thus
arithmetic involving pointers and integers does not translate to
arithmetic over the integer representation of a pointer.

With the recently added bounds checks on pointers involved in arithmetic
we have a more reliable way of testing for overflow in pointer
arithmetic.

Author: tautschnig

regression/cbmc-library/getenv-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---signed-overflow-check --unsigned-overflow-check
+--signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --pointer-check --bounds-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/pointer-overflow1/test.desc

@@ -3,12 +3,14 @@ main.c
 --pointer-overflow-check --unsigned-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.overflow\.\d+\] line 8 (pointer )?arithmetic overflow on .*: FAILURE
-^\[main\.overflow\.\d+\] line 9 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 8 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 9 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
 ^\[main\.overflow\.\d+\] line 10 (pointer )?arithmetic overflow on .*: FAILURE
-^\[main\.overflow\.\d+\] line 11 (pointer )?arithmetic overflow on .*: FAILURE
-^\[main\.overflow\.\d+\] line 12 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 10 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 11 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 12 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
 ^VERIFICATION FAILED$
 --
 ^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
+^\[main\.overflow\.\d+\] line 1[45] pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
 ^warning: ignoring

regression/cbmc/pointer-overflow2/test.desc

@@ -3,9 +3,9 @@ main.c
 --pointer-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.overflow.1\] line \d+ pointer arithmetic overflow on - in p - \(signed long (long )?int\)1: SUCCESS
-\[main.overflow.2\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long (long )?int\)1: SUCCESS
-\[main.overflow.3\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long (long )?int\)-1: SUCCESS
-\[main.overflow.4\] line \d+ pointer arithmetic overflow on - in p - \(signed long (long )?int\)-1: SUCCESS
+\[main.pointer_arithmetic.1\] line \d+ pointer arithmetic: invalid integer address in p - \(signed long (long )?int\)1: SUCCESS
+\[main.pointer_arithmetic.2\] line \d+ pointer arithmetic: invalid integer address in p \+ \(signed long (long )?int\)1: SUCCESS
+\[main.pointer_arithmetic.3\] line \d+ pointer arithmetic: invalid integer address in p \+ \(signed long (long )?int\)-1: SUCCESS
+\[main.pointer_arithmetic.4\] line \d+ pointer arithmetic: invalid integer address in p - \(signed long (long )?int\)-1: SUCCESS
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -1177,22 +1177,6 @@ void goto_checkt::pointer_overflow_check(
     expr.operands().size() == 2,
     "pointer arithmetic expected to have exactly 2 operands");
 
-  // check for address space overflow by checking for overflow on integers
-  exprt overflow("overflow-" + expr.id_string(), bool_typet());
-  for(const auto &op : expr.operands())
-  {
-    overflow.add_to_operands(
-      typecast_exprt::conditional_cast(op, pointer_diff_type()));
-  }
-
-  add_guarded_property(
-    not_exprt(overflow),
-    "pointer arithmetic overflow on " + expr.id_string(),
-    "overflow",
-    expr.find_source_location(),
-    expr,
-    guard);
-
   // the result must be within object bounds or one past the end
   const auto size = from_integer(0, size_type());
   auto conditions = get_pointer_dereferenceable_conditions(expr, size);