Pointer arithmetic overflow is overflow on integer representation

At a bare minimum, we should report an overflow when performing pointer
arithmetic that would result in an overflow on the underlying integer
representation.

As future work, we may want to expand on those checks by reporting
overflows when exceeding object bounds, as discussed in diffblue#5426.

Fixes: diffblue#5284

Author: tautschnig

regression/cbmc/pointer-overflow2/test.desc

@@ -1,11 +1,11 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.overflow.1\] line \d+ pointer arithmetic overflow on - in p - \(signed long int\)1: SUCCESS
-\[main.overflow.2\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long int\)1: SUCCESS
-\[main.overflow.3\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long int\)-1: SUCCESS
-\[main.overflow.4\] line \d+ pointer arithmetic overflow on - in p - \(signed long int\)-1: SUCCESS
+\[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
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -1157,8 +1157,13 @@ 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());
-  overflow.operands() = expr.operands();
+  for(const auto &op : expr.operands())
+  {
+    overflow.add_to_operands(
+      typecast_exprt::conditional_cast(op, pointer_diff_type()));
+  }
 
   add_guarded_property(
     not_exprt(overflow),