Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1255,11 +1255,11 @@ struct
else
st

let threadenter =
let threadenter ask st =
if Param.side_effect_global_init then
startstate_threadenter startstate
startstate_threadenter startstate ask st
else
old_threadenter
{(old_threadenter ask st) with priv = W.empty ()}
end

module LockCenteredD =
Expand Down
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); // used to spuriously publish 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); // used to pass g = 8 and W: A -> {g} to t_fun2
g = 0;
pthread_mutex_unlock(&A);

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