Merge pull request #303 from danpoe/concurrency-regression-tests

Two concurrency regression tests for cbmc

Author: Daniel Kroening

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;
+}
+

regression/cbmc-concurrency/global_pointer1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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;
+}

regression/cbmc-concurrency/stack1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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;
 }