From f27b0983fbb667528c3939da5d5299350b11c286 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 13 Oct 2023 17:28:53 +0300 Subject: [PATCH] Add Freiburg case_distinction_with_ghosts example --- .../64-case_distinction_with_ghosts.c | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 tests/regression/46-apron2/64-case_distinction_with_ghosts.c diff --git a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c new file mode 100644 index 0000000000..06df245afd --- /dev/null +++ b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c @@ -0,0 +1,39 @@ +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +#include +#include + +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(g != 1 || x >= 42); + __VERIFIER_atomic_end(); + } + + return 0; +} + +int main() +{ + pthread_t tid; + pthread_create(&tid, 0, inc, 0); + __VERIFIER_atomic_begin(); + g = 1; x = 42; + __VERIFIER_atomic_end(); + + assert(x >= 42); + return 0; +}