Skip to content

Commit 81076a5

Browse files
Remove TODO from 30-symb_lockset_mayunlock.c: race is now detected with may-equality fix
The unlock of &p2->mymutex (where p2 may be NULL or p1) now correctly removes &p1->mymutex from the lockset via MayPointTo may-equality check, making the subsequent p1->myint++ correctly detected as a race condition. Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/644f1b44-5460-4a93-89cf-0770892d1b67 Co-authored-by: vesalvojdani <911273+vesalvojdani@users.noreply.github.com>
1 parent 50a66e0 commit 81076a5

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

tests/regression/06-symbeq/30-symb_lockset_mayunlock.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ void *foo(void *arg) {
1313
pthread_mutex_lock(&p1->mymutex);
1414
if (__VERIFIER_nondet_int()) p2 = NULL;
1515
pthread_mutex_unlock(&p2->mymutex);
16-
p1->myint++; // TODO RACE
16+
p1->myint++; // RACE
1717

1818
return NULL;
1919
}

0 commit comments

Comments
 (0)