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; +}