diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 6c330e8798..31dd1fc4f5 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -864,7 +864,7 @@ struct let get_relevant_writes (ask:Q.ask) m v = let current = Digest.current ask in GMutex.fold (fun k v acc -> - if Digest.accounted_for ask ~current ~other:k then + if not (Digest.accounted_for ask ~current ~other:k) then LRD.join acc (Cluster.keep_only_protected_globals ask m v) else acc diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 26fb5850a8..20ef13244b 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -425,7 +425,7 @@ struct let current = Digest.current ask in let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in GMutex.fold (fun k v acc -> - if Digest.accounted_for ask ~current ~other:k then + if not (Digest.accounted_for ask ~current ~other:k) then CPA.join acc (CPA.filter is_in_Gm v) else acc diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 5f89eecdd8..2739578957 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -175,14 +175,14 @@ struct match current, other with | `Lifted current, `Lifted other -> if TID.is_unique current && TID.equal current other then - false (* self-read *) + true (* self-read *) else if GobConfig.get_bool "ana.relation.priv.not-started" && MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other then - false (* other is not started yet *) + true (* other is not started yet *) else if GobConfig.get_bool "ana.relation.priv.must-joined" && MHP.must_be_joined other (ask.f Queries.MustJoinedThreads) then - false (* accounted for in local information *) + true (* accounted for in local information *) else - true - | _ -> true + false + | _ -> false end module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) = @@ -247,7 +247,7 @@ struct let get_relevant_writes_nofilter (ask:Q.ask) v = let current = Digest.current ask in GMutex.fold (fun k v acc -> - if Digest.accounted_for ask ~current ~other:k then + if not (Digest.accounted_for ask ~current ~other:k) then LD.join acc v else acc