Skip to content

Commit ba39674

Browse files
committed
Add mine-W-noinit test for resetting W in threadenter
1 parent b68df11 commit ba39674

1 file changed

Lines changed: 32 additions & 0 deletions

File tree

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// PARAM: --set ana.base.privatization mine-W-noinit --enable ana.int.enums
2+
#include <pthread.h>
3+
#include <goblint.h>
4+
5+
int g;
6+
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
7+
8+
void *t_fun(void *arg) {
9+
return NULL;
10+
}
11+
12+
void *t_fun2(void *arg) {
13+
pthread_mutex_lock(&A);
14+
pthread_mutex_unlock(&A); // spuriously publishes g = 8
15+
return NULL;
16+
}
17+
18+
int main() {
19+
pthread_t id, id2;
20+
pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
21+
22+
pthread_mutex_lock(&A);
23+
g = 8;
24+
pthread_create(&id2, NULL, t_fun2, NULL); // passes g = 8 and W: A -> {g} to t_fun2
25+
g = 0;
26+
pthread_mutex_unlock(&A);
27+
28+
pthread_mutex_lock(&A);
29+
__goblint_check(g == 0); // TODO
30+
pthread_mutex_unlock(&A);
31+
return 0;
32+
}

0 commit comments

Comments
 (0)