From 696a35ff9a232bb48353e6ddefeca5398e92d6a2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 16:58:11 +0200 Subject: [PATCH] Comment out atomic mutex protecting everything again --- src/analyses/mutexAnalysis.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 702b3b4224..a0f4304b54 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -229,9 +229,9 @@ struct let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) - if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then + (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then true - else + else *) Mutexes.leq mutex_lockset protecting | Queries.MustLockset -> let held_locks = Lockset.export_locks (Lockset.filter snd ls) in