Regression tests demonstrating spurious pointer overflow check failure

Author: danpoe

regression/cbmc/pointer-overflow2/main.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+
+void main()
+{
+  char *p = (char *)10;
+  p -= 1;
+  p += 1;
+  p += -1; // spurious pointer overflow report
+  p -= -1; // spurious pointer overflow report
+}

regression/cbmc/pointer-overflow2/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+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
+--
+^warning: ignoring