Skip to content

Commit 284fcfc

Browse files
Add regression test for pthread argument escape in region analysis
Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/564e520d-ac51-4680-9e7c-99ad250e4cca Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent d26f8fb commit 284fcfc

1 file changed

Lines changed: 28 additions & 0 deletions

File tree

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// PARAM: --set ana.activated[+] "'region'"
2+
// Regression: pthread argument properly tracked as escaped in region analysis.
3+
// The region analysis must treat a local variable passed via pthread argument
4+
// as escaped (global), enabling proper race detection.
5+
// The NORACE variant (same mutex) shows no false positives.
6+
// See also 09/34 which is the RACE variant with different mutexes.
7+
#include <pthread.h>
8+
9+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
10+
11+
void *t_fun(void *arg) {
12+
int *p = (int *) arg;
13+
pthread_mutex_lock(&mutex);
14+
(*p)++; // NORACE
15+
pthread_mutex_unlock(&mutex);
16+
return NULL;
17+
}
18+
19+
int main(void) {
20+
pthread_t id;
21+
int i;
22+
pthread_create(&id, NULL, t_fun, (void *) &i);
23+
pthread_mutex_lock(&mutex);
24+
i++; // NORACE
25+
pthread_mutex_unlock(&mutex);
26+
pthread_join(id, NULL);
27+
return 0;
28+
}

0 commit comments

Comments
 (0)