Merge branch 'master' into fix-apron-overflows

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 =

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 <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;
+}