From 4e7312b45d3b0956db71756a5d5e45d5bb22ccfd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 13 Oct 2023 17:40:47 +0300 Subject: [PATCH] Add simpler case_distinction tests --- .../64-case_distinction_with_ghosts.c | 4 +-- .../65-case_distinction_with_ghosts-2.c | 30 +++++++++++++++++++ .../66-case_distinction_with_ghosts-3.c | 30 +++++++++++++++++++ 3 files changed, 62 insertions(+), 2 deletions(-) create mode 100644 tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c create mode 100644 tests/regression/46-apron2/66-case_distinction_with_ghosts-3.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 index 06df245afd..633c1192c9 100644 --- a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c +++ b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c @@ -19,7 +19,7 @@ void* inc() __VERIFIER_atomic_end(); __VERIFIER_atomic_begin(); - assert(g != 1 || x >= 42); + assert(g != 1 || x >= 42); // TODO __VERIFIER_atomic_end(); } @@ -34,6 +34,6 @@ int main() g = 1; x = 42; __VERIFIER_atomic_end(); - assert(x >= 42); + assert(x >= 42); // TODO return 0; } diff --git a/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c new file mode 100644 index 0000000000..89371e74fa --- /dev/null +++ b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c @@ -0,0 +1,30 @@ +// 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(g != 1 || x >= 42); // TODO + __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); // TODO + return 0; +} diff --git a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c new file mode 100644 index 0000000000..6fc2700299 --- /dev/null +++ b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c @@ -0,0 +1,30 @@ +// 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() +{ + // x = 10; // TODO: what is this? + + __VERIFIER_atomic_begin(); + assert(g != 1 || x >= 42); // TODO + __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(); + return 0; +}