From 78a84849a019f39533d53be94c6c83871e583635 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:01:12 +0200 Subject: [PATCH] Add lock-digest example from more-traces --- tests/regression/46-apron2/58-lock-digest.c | 36 +++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 tests/regression/46-apron2/58-lock-digest.c diff --git a/tests/regression/46-apron2/58-lock-digest.c b/tests/regression/46-apron2/58-lock-digest.c new file mode 100644 index 0000000000..c77c1ab821 --- /dev/null +++ b/tests/regression/46-apron2/58-lock-digest.c @@ -0,0 +1,36 @@ +// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// TODO: why does this work? even with earlyglobs +#include +#include + +int g, h; +pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; + +void *t2(void *arg) { + pthread_mutex_lock(&a); + __goblint_check(h <= g); // TODO: should be h < g? + pthread_mutex_unlock(&a); + return NULL; +} + +void *t1(void *arg) { + pthread_t x; + pthread_create(&x, NULL, t2, NULL); + + pthread_mutex_lock(&a); + h = 11; g = 12; + pthread_mutex_unlock(&a); + + return NULL; +} + +int main() { + pthread_mutex_lock(&a); + h = 9; + g = 10; + pthread_mutex_unlock(&a); + + pthread_t x; + pthread_create(&x, NULL, t1, NULL); + return 0; +}