more

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2320 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc-concurrency/atomic_section_sc1/main.c

@@ -0,0 +1,12 @@
+int global;
+
+int main()
+{
+  __CPROVER_ASYNC_1: global=2;
+
+  __CPROVER_ATOMIC_BEGIN();
+  global=1;
+  // no interleaving here
+  assert(global==1);
+  __CPROVER_ATOMIC_END();
+}

regression/cbmc-concurrency/atomic_section_sc1/test.desc

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

regression/cbmc-concurrency/atomic_section_sc2/main.c

@@ -0,0 +1,14 @@
+int global;
+
+int main()
+{
+  global=1;
+
+  __CPROVER_ASYNC_1: assert(global==1);
+
+  __CPROVER_ATOMIC_BEGIN();
+  global=2;
+  // no interleaving here
+  global=1;
+  __CPROVER_ATOMIC_END();
+}

regression/cbmc-concurrency/atomic_section_sc2/test.desc

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

regression/cbmc-concurrency/sc5/main.c

@@ -0,0 +1,17 @@
+int global;
+
+void thread()
+{
+  global=1;
+  global=2;
+}
+
+int main()
+{
+  __CPROVER_ASYNC_1: thread();
+
+  if(global==2)
+  {
+    assert(global!=1);
+  }
+}

regression/cbmc-concurrency/sc5/test.desc

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