From be4d3de02fba0cc16bfc8cc3072893b0d3516d6e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 Dec 2024 17:42:49 +0200
Subject: [PATCH] Fix mine-W-noinit threadenter to reset W

---
 src/analyses/basePriv.ml                               | 6 +++---
 tests/regression/13-privatized/96-mine-W-threadenter.c | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

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
index 424d45c52b..ec9903b653 100644
--- a/tests/regression/13-privatized/96-mine-W-threadenter.c
+++ b/tests/regression/13-privatized/96-mine-W-threadenter.c
@@ -11,7 +11,7 @@ void *t_fun(void *arg) {
 
 void *t_fun2(void *arg) {
   pthread_mutex_lock(&A);
-  pthread_mutex_unlock(&A); // spuriously publishes g = 8
+  pthread_mutex_unlock(&A); // used to spuriously publish g = 8
   return NULL;
 }
 
@@ -21,12 +21,12 @@ int main() {
 
   pthread_mutex_lock(&A);
   g = 8;
-  pthread_create(&id2, NULL, t_fun2, NULL); // passes g = 8 and W: A -> {g} to t_fun2
+  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); // TODO
+  __goblint_check(g == 0);
   pthread_mutex_unlock(&A);
   return 0;
 }