From 29df7ecaa3d34a8e21f66a9b77a56d9db74a03f4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Mar 2024 10:41:33 +0200 Subject: [PATCH] Make 46-apron2/80-lock-digest pass with mutex-meet-tid --- tests/regression/46-apron2/80-lock-digest.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/regression/46-apron2/80-lock-digest.c b/tests/regression/46-apron2/80-lock-digest.c index 826d4f3b41..02adf8116d 100644 --- a/tests/regression/46-apron2/80-lock-digest.c +++ b/tests/regression/46-apron2/80-lock-digest.c @@ -1,4 +1,5 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --set ana.path_sens[+] threadflag +// cherry-picked from https://github.com/goblint/analyzer/pull/1286: works with mutex-meet-tid, without lock digests #include #include @@ -8,7 +9,7 @@ pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; void *t2(void *arg) { pthread_mutex_lock(&a); // wrong in more-traces! - __goblint_check(h < g); // TODO + __goblint_check(h < g); pthread_mutex_unlock(&a); return NULL; }