Add Freiburg nondet_inc_with_ghosts examples

tests/regression/46-apron2/67-nondet_inc_with_ghosts.c

@@ -0,0 +1,43 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(x >= g); // TODO
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}

tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c

@@ -0,0 +1,38 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  x++;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  assert(x >= g); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}

tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c

@@ -0,0 +1,34 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  assert(x >= g);
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}