Merge pull request #5814 from tautschnig/pointer-overflow-check

Pointer arithmetic overflow is overflow on integer representation

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),