@@ -279,12 +279,12 @@ struct
279279 if Locksets. (not (Lockset. mem m (current_lockset ask))) then (
280280 let get_m = get_m_with_mutex_inits ask getg m in
281281 (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
282- where our (necessary) original context still has the mutex,
283- so the query would be on the wrong lockset.
284- TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
285- Therefore, just use _without to exclude the mutex we shouldn't have.
286- In non-cond locks we don't have it anyway, so there's no difference.
287- No other privatization uses is_unprotected, so this hack is only needed here. *)
282+ where our (necessary) original context still has the mutex,
283+ so the query would be on the wrong lockset.
284+ TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
285+ Therefore, just use _without to exclude the mutex we shouldn't have.
286+ In non-cond locks we don't have it anyway, so there's no difference.
287+ No other privatization uses is_unprotected, so this hack is only needed here. *)
288288 let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
289289 let cpa' = CPA. filter is_in_V get_m in
290290 if M. tracing then M. tracel " priv" " PerMutexOplusPriv.lock m=%a cpa'=%a\n " LockDomain.Addr. pretty m CPA. pretty cpa';
0 commit comments