Output unprotected invariants from vojdani privatization

goblint · Jan 13, 2025 · dc678ab · dc678ab
1 parent 8f4048e
commit dc678ab
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
@@ -831,7 +831,7 @@ struct
 
   let invariant_global (ask: Q.ask) getg g =
     let locks = ask.f (Q.MustProtectingLocks {global = g; write = false}) in
-    if LockDomain.MustLockset.is_all locks || LockDomain.MustLockset.is_empty locks then (* TODO: output unprotected invariant with empty lockset? *)
+    if LockDomain.MustLockset.is_all locks then
       Invariant.none
     else (
       let read_global g = getg g in (* TODO: read top for others? or at least those which might not have all same protecting locks? *)