Fix mine-W-noinit threadenter to reset W

goblint · Dec 16, 2024 · be4d3de · be4d3de
1 parent ba39674
commit be4d3de
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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;
 }