Skip to content

Commit

Permalink
Add lock-digest example from more-traces
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Nov 30, 2023
1 parent 05198f9 commit 78a8484
Showing 1 changed file with 36 additions and 0 deletions.
36 changes: 36 additions & 0 deletions tests/regression/46-apron2/58-lock-digest.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet
// TODO: why does this work? even with earlyglobs
#include <pthread.h>
#include <goblint.h>

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

0 comments on commit 78a8484

Please sign in to comment.