Skip to content

Commit

Permalink
Add ex-10 from traces
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Dec 16, 2024
1 parent b7747c9 commit 48ba6af
Showing 1 changed file with 30 additions and 0 deletions.
30 changes: 30 additions & 0 deletions tests/regression/13-privatized/89-traces-ex-10.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
#include <pthread.h>
#include <goblint.h>

int g = 7; // matches precise read
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
pthread_mutex_lock(&A);
pthread_mutex_lock(&B);
g = 42;
pthread_mutex_unlock(&B);
g = 7;
pthread_mutex_unlock(&A);
return NULL;
}

int main(void) {
pthread_t id;
pthread_create(&id, NULL, t_fun, NULL);

pthread_mutex_lock(&B);
// __goblint_check(g == 7); // UNKNOWN!
pthread_mutex_unlock(&B);

pthread_mutex_lock(&A);
pthread_mutex_lock(&B);
__goblint_check(g == 7);
return 0;
}

0 comments on commit 48ba6af

Please sign in to comment.