From 27854b4e7c619f1145a5cd933a4f65268d731d49 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@cs.ox.ac.uk>
Date: Mon, 14 Nov 2016 12:26:51 +0000
Subject: [PATCH] two new cbmc concurrency regression tests

---
 .../cbmc-concurrency/global_pointer1/main.c   | 33 +++++++++++++++++++
 .../global_pointer1/test.desc                 |  8 +++++
 regression/cbmc-concurrency/stack1/main.c     | 23 +++++++++++++
 regression/cbmc-concurrency/stack1/test.desc  |  8 +++++
 .../cbmc-concurrency/struct_and_array1/main.c |  2 +-
 5 files changed, 73 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc-concurrency/global_pointer1/main.c
 create mode 100644 regression/cbmc-concurrency/global_pointer1/test.desc
 create mode 100644 regression/cbmc-concurrency/stack1/main.c
 create mode 100644 regression/cbmc-concurrency/stack1/test.desc

diff --git a/regression/cbmc-concurrency/global_pointer1/main.c b/regression/cbmc-concurrency/global_pointer1/main.c
new file mode 100644
index 00000000000..604e94f181a
--- /dev/null
+++ b/regression/cbmc-concurrency/global_pointer1/main.c
@@ -0,0 +1,33 @@
+#include <pthread.h>
+#include <assert.h>
+
+int *v;
+int g;
+
+void *thread1(void * arg)
+{
+  v = &g;
+}
+
+void *thread2(void *arg)
+{
+  assert(v == &g);
+  *v = 1;
+}
+
+int main()
+{
+  pthread_t t1, t2;
+
+  pthread_create(&t1, 0, thread1, 0);
+  pthread_join(t1, 0);
+
+  pthread_create(&t2, 0, thread2, 0);
+  pthread_join(t2, 0);
+
+  assert(v == &g);
+  assert(*v == 1);
+
+  return 0;
+}
+
diff --git a/regression/cbmc-concurrency/global_pointer1/test.desc b/regression/cbmc-concurrency/global_pointer1/test.desc
new file mode 100644
index 00000000000..52168c7eba4
--- /dev/null
+++ b/regression/cbmc-concurrency/global_pointer1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/stack1/main.c b/regression/cbmc-concurrency/stack1/main.c
new file mode 100644
index 00000000000..b4fcad2afaa
--- /dev/null
+++ b/regression/cbmc-concurrency/stack1/main.c
@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <assert.h>
+
+void *thread(void *arg)
+{
+  int *i = (int *)arg;
+  *i = 1;
+}
+
+int main(void)
+{
+  int x;
+  x = 0;
+
+  pthread_t t;
+
+  pthread_create(&t, NULL, thread, &x);
+  pthread_join(t, NULL);
+
+  assert(x == 1);
+
+  return 0;
+}
diff --git a/regression/cbmc-concurrency/stack1/test.desc b/regression/cbmc-concurrency/stack1/test.desc
new file mode 100644
index 00000000000..52168c7eba4
--- /dev/null
+++ b/regression/cbmc-concurrency/stack1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-concurrency/struct_and_array1/main.c b/regression/cbmc-concurrency/struct_and_array1/main.c
index 42164904232..fdc909d823b 100644
--- a/regression/cbmc-concurrency/struct_and_array1/main.c
+++ b/regression/cbmc-concurrency/struct_and_array1/main.c
@@ -22,7 +22,7 @@ void *foo1(void *arg1)
 void *foo2(void *arg2)
 {
   st.y = 1;
-  my_array[2]=2;
+  my_array[2]=1;
   done2 = 1;
 }