diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 3afd758daa..792f084e05 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -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 = diff --git a/tests/regression/13-privatized/96-mine-W-threadenter.c b/tests/regression/13-privatized/96-mine-W-threadenter.c new file mode 100644 index 0000000000..ec9903b653 --- /dev/null +++ b/tests/regression/13-privatized/96-mine-W-threadenter.c @@ -0,0 +1,32 @@ +// PARAM: --set ana.base.privatization mine-W-noinit --enable ana.int.enums +#include +#include + +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; +}