From 4c541403006dfd48311435362e2707e42262e608 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 20 Oct 2023 11:56:56 +0300 Subject: [PATCH] Add Freiburg nondet_inc_with_ghosts examples --- .../46-apron2/67-nondet_inc_with_ghosts.c | 43 +++++++++++++++++++ .../46-apron2/68-nondet_inc_with_ghosts-2.c | 38 ++++++++++++++++ .../46-apron2/69-nondet_inc_with_ghosts-3.c | 34 +++++++++++++++ 3 files changed, 115 insertions(+) create mode 100644 tests/regression/46-apron2/67-nondet_inc_with_ghosts.c create mode 100644 tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c create mode 100644 tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c new file mode 100644 index 0000000000..cfbab7f922 --- /dev/null +++ b/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 +#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(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; +} diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c new file mode 100644 index 0000000000..3d41428a59 --- /dev/null +++ b/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 +#include + +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; +} diff --git a/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c new file mode 100644 index 0000000000..0519dbda00 --- /dev/null +++ b/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 +#include + +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; +}