Skip to content

Commit

Permalink
Add mine-W-noinit test for resetting W in threadenter
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Dec 16, 2024
1 parent b68df11 commit ba39674
Showing 1 changed file with 32 additions and 0 deletions.
32 changes: 32 additions & 0 deletions tests/regression/13-privatized/96-mine-W-threadenter.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
// PARAM: --set ana.base.privatization mine-W-noinit --enable ana.int.enums
#include <pthread.h>
#include <goblint.h>

int g;
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
return NULL;
}

void *t_fun2(void *arg) {
pthread_mutex_lock(&A);
pthread_mutex_unlock(&A); // spuriously publishes g = 8
return NULL;
}

int main() {
pthread_t id, id2;
pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded

pthread_mutex_lock(&A);
g = 8;
pthread_create(&id2, NULL, t_fun2, NULL); // passes g = 8 and W: A -> {g} to t_fun2
g = 0;
pthread_mutex_unlock(&A);

pthread_mutex_lock(&A);
__goblint_check(g == 0); // TODO
pthread_mutex_unlock(&A);
return 0;
}

0 comments on commit ba39674

Please sign in to comment.