From 61768113d451956ee451cbb76e39b76f34e99341 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 16 Feb 2019 16:43:10 +0000
Subject: [PATCH] Add tests for overflows

There is an interaction between type promotion and
overflow detection. In the case of compound assignments
type promotion is broken.
---
 regression/cbmc/Overflow_Addition2/main.c    |  6 ++++++
 regression/cbmc/Overflow_Addition2/test.desc |  9 +++++++++
 regression/cbmc/Overflow_Addition3/main.c    |  6 ++++++
 regression/cbmc/Overflow_Addition3/test.desc | 15 +++++++++++++++
 regression/cbmc/Overflow_Addition4/main.c    |  6 ++++++
 regression/cbmc/Overflow_Addition4/test.desc | 13 +++++++++++++
 6 files changed, 55 insertions(+)
 create mode 100644 regression/cbmc/Overflow_Addition2/main.c
 create mode 100644 regression/cbmc/Overflow_Addition2/test.desc
 create mode 100644 regression/cbmc/Overflow_Addition3/main.c
 create mode 100644 regression/cbmc/Overflow_Addition3/test.desc
 create mode 100644 regression/cbmc/Overflow_Addition4/main.c
 create mode 100644 regression/cbmc/Overflow_Addition4/test.desc

diff --git a/regression/cbmc/Overflow_Addition2/main.c b/regression/cbmc/Overflow_Addition2/main.c
new file mode 100644
index 00000000000..c75ed765604
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition2/main.c
@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i++;
+}
diff --git a/regression/cbmc/Overflow_Addition2/test.desc b/regression/cbmc/Overflow_Addition2/test.desc
new file mode 100644
index 00000000000..2615a9d290d
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition2/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Overflow_Addition3/main.c b/regression/cbmc/Overflow_Addition3/main.c
new file mode 100644
index 00000000000..0a4c6ec4e5c
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition3/main.c
@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i += 1;
+}
diff --git a/regression/cbmc/Overflow_Addition3/test.desc b/regression/cbmc/Overflow_Addition3/test.desc
new file mode 100644
index 00000000000..30ddc3b3ab4
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition3/test.desc
@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS
+^\[.*\] .* arithmetic overflow on signed type conversion in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The addition is done in signed int; hence, the overflow is only detected
+on conversion.
+
+See #4208.
diff --git a/regression/cbmc/Overflow_Addition4/main.c b/regression/cbmc/Overflow_Addition4/main.c
new file mode 100644
index 00000000000..aee20d618cb
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition4/main.c
@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i = i + 1;
+}
diff --git a/regression/cbmc/Overflow_Addition4/test.desc b/regression/cbmc/Overflow_Addition4/test.desc
new file mode 100644
index 00000000000..56da91e2003
--- /dev/null
+++ b/regression/cbmc/Overflow_Addition4/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS
+^\[.*\] .* arithmetic overflow on signed type conversion in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The addition is done in signed int; hence, the overflow is only detected
+on conversion.