Skip to content

Commit dc678ab

Browse files
committed
Output unprotected invariants from vojdani privatization
1 parent 8f4048e commit dc678ab

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/analyses/basePriv.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -831,7 +831,7 @@ struct
831831

832832
let invariant_global (ask: Q.ask) getg g =
833833
let locks = ask.f (Q.MustProtectingLocks {global = g; write = false}) in
834-
if LockDomain.MustLockset.is_all locks || LockDomain.MustLockset.is_empty locks then (* TODO: output unprotected invariant with empty lockset? *)
834+
if LockDomain.MustLockset.is_all locks then
835835
Invariant.none
836836
else (
837837
let read_global g = getg g in (* TODO: read top for others? or at least those which might not have all same protecting locks? *)

0 commit comments

Comments
 (0)