From b12b6e83f70cda82af11c0065c3631228180b59e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 16:44:27 +0200 Subject: [PATCH] Delete duplicate priv-atomic tests --- .../66-case_distinction_with_ghosts-3.c | 30 -------- .../46-apron2/74-mutex_with_ghosts-3.c | 1 + .../46-apron2/75-mutex_with_ghosts-4.c | 69 ------------------- 3 files changed, 1 insertion(+), 99 deletions(-) delete mode 100644 tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c delete mode 100644 tests/regression/46-apron2/75-mutex_with_ghosts-4.c 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 deleted file mode 100644 index e130c68fa1..0000000000 --- a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c +++ /dev/null @@ -1,30 +0,0 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --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; -} diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c index a1c83950b5..e7da4cb5bc 100644 --- a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c +++ b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c @@ -1,4 +1,5 @@ // PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening +// TODO: unsound with cluster12 /*----------------------------------------------------------------------------- * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for * witness validation using locking to access a shared diff --git a/tests/regression/46-apron2/75-mutex_with_ghosts-4.c b/tests/regression/46-apron2/75-mutex_with_ghosts-4.c deleted file mode 100644 index ff544708e1..0000000000 --- a/tests/regression/46-apron2/75-mutex_with_ghosts-4.c +++ /dev/null @@ -1,69 +0,0 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening -// TODO: unsound with cluster12 -/*----------------------------------------------------------------------------- - * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for - * witness validation using locking to access a shared - * variable - *----------------------------------------------------------------------------- - * Author: Frank Schüssele - * Date: 2023-07-11 - *---------------------------------------------------------------------------*/ -#include -#include - -extern void __VERIFIER_atomic_begin(); -extern void __VERIFIER_atomic_end(); - -int used; -int g = 0; -pthread_mutex_t m; - -void* producer() -{ - while (1) { - __VERIFIER_atomic_begin(); - g = 1; - pthread_mutex_lock(&m); - __VERIFIER_atomic_end(); - - used++; - used--; - - __VERIFIER_atomic_begin(); - g = 0; - pthread_mutex_unlock(&m); - __VERIFIER_atomic_end(); - } - - return 0; -} - -int main() -{ - pthread_t tid; - - pthread_mutex_init(&m, 0); - pthread_create(&tid, 0, producer, 0); - - __VERIFIER_atomic_begin(); - int g2 = g; - int used2 = used; - __goblint_check(used2 == 0); // UNKNOWN! (currently unsound) - __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?) - __VERIFIER_atomic_end(); - - __VERIFIER_atomic_begin(); - g = 1; - pthread_mutex_lock(&m); - __VERIFIER_atomic_end(); - - __goblint_check(used == 0); - - __VERIFIER_atomic_begin(); - g = 0; - pthread_mutex_unlock(&m); - __VERIFIER_atomic_end(); - - pthread_mutex_destroy(&m); - return 0; -}