Skip to content

Commit 48ba6af

Browse files
committed
Add ex-10 from traces
1 parent b7747c9 commit 48ba6af

File tree

1 file changed

+30
-0
lines changed

1 file changed

+30
-0
lines changed
Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <pthread.h>
2+
#include <goblint.h>
3+
4+
int g = 7; // matches precise read
5+
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
7+
8+
void *t_fun(void *arg) {
9+
pthread_mutex_lock(&A);
10+
pthread_mutex_lock(&B);
11+
g = 42;
12+
pthread_mutex_unlock(&B);
13+
g = 7;
14+
pthread_mutex_unlock(&A);
15+
return NULL;
16+
}
17+
18+
int main(void) {
19+
pthread_t id;
20+
pthread_create(&id, NULL, t_fun, NULL);
21+
22+
pthread_mutex_lock(&B);
23+
// __goblint_check(g == 7); // UNKNOWN!
24+
pthread_mutex_unlock(&B);
25+
26+
pthread_mutex_lock(&A);
27+
pthread_mutex_lock(&B);
28+
__goblint_check(g == 7);
29+
return 0;
30+
}

0 commit comments

Comments
 (0)