regression tests for diffblue#123

Author: Peter Schrammel

regression/cbmc-concurrency/norace_array1/main.c

@@ -0,0 +1,26 @@
+#include <pthread.h>
+#include <assert.h>
+
+int s[2];
+
+void* thread_0(void* arg)
+{
+  s[0] = 2;
+  assert(s[0] == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s[1] = 1;
+  assert(s[1] == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}

regression/cbmc-concurrency/norace_array1/test.desc

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

regression/cbmc-concurrency/norace_scalar1/main.c

@@ -0,0 +1,26 @@
+#include <pthread.h>
+#include <assert.h>
+
+int f0, f1;
+
+void* thread_0(void* arg)
+{
+  f0 = 2;
+  assert(f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  f1 = 1;
+  assert(f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}

regression/cbmc-concurrency/norace_scalar1/test.desc

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

regression/cbmc-concurrency/norace_struct1/main.c

@@ -0,0 +1,26 @@
+#include <pthread.h>
+#include <assert.h>
+
+struct { int f0; int f1; } s;
+
+void* thread_0(void* arg)
+{
+  s.f0 = 2;
+  assert(s.f0 == 2);
+  return NULL;
+}
+
+void* thread_1(void* arg)
+{
+  s.f1 = 1;
+  assert(s.f1 == 1);
+  return NULL;
+}
+
+int main(void)
+{
+  pthread_t thread0, thread1;
+  pthread_create(&thread0, NULL, thread_0, 0);
+  pthread_create(&thread1, NULL, thread_1, 0);
+  return 0;
+}

regression/cbmc-concurrency/norace_struct1/test.desc

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