From 0c8aedd4aa5542502164fb704583b84a215a22f1 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Tue, 31 Mar 2020 19:12:57 +0100
Subject: [PATCH] Regression tests demonstrating spurious pointer overflow
 check failure

---
 regression/cbmc/pointer-overflow2/main.c    | 10 ++++++++++
 regression/cbmc/pointer-overflow2/test.desc | 11 +++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc/pointer-overflow2/main.c
 create mode 100644 regression/cbmc/pointer-overflow2/test.desc

diff --git a/regression/cbmc/pointer-overflow2/main.c b/regression/cbmc/pointer-overflow2/main.c
new file mode 100644
index 00000000000..e73ba1eb115
--- /dev/null
+++ b/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
+}
diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc
new file mode 100644
index 00000000000..0cd1d164728
--- /dev/null
+++ b/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