diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 7d06844c1b..db75455b40 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -60,15 +60,10 @@ struct ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection}) let protected_vars (ask: Q.ask): varinfo list = - let module VS = Set.Make (CilType.Varinfo) in Q.AD.fold (fun m acc -> - Q.AD.fold (fun l acc -> - match l with - | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *) - | _ -> acc - ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc - ) (ask.f Q.MustLockset) VS.empty - |> VS.elements + Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc + ) (ask.f Q.MustLockset) (Q.VS.empty ()) + |> Q.VS.elements end module MutexGlobals = diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9cc019db76..5a61976ef5 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -240,8 +240,8 @@ struct | Queries.MustProtectedVars {mutex = m; write} -> let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in VarSet.fold (fun v acc -> - Queries.AD.join (Queries.AD.of_var v) acc - ) protected (Queries.AD.empty ()) + Queries.VS.add v acc + ) protected (Queries.VS.empty ()) | Queries.IterSysVars (Global g, f) -> f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *) | WarnGlobal g -> diff --git a/src/domains/queries.ml b/src/domains/queries.ml index e51ee90f68..3a0e493640 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -114,7 +114,7 @@ type _ t = | CreatedThreads: ConcDomain.ThreadSet.t t | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t - | MustProtectedVars: mustprotectedvars -> AD.t t + | MustProtectedVars: mustprotectedvars -> VS.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) @@ -179,7 +179,7 @@ struct | CreatedThreads -> (module ConcDomain.ThreadSet) | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) - | MustProtectedVars _ -> (module AD) + | MustProtectedVars _ -> (module VS) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) | WarnGlobal _ -> (module Unit) @@ -243,7 +243,7 @@ struct | CreatedThreads -> ConcDomain.ThreadSet.top () | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () - | MustProtectedVars _ -> AD.top () + | MustProtectedVars _ -> VS.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () | WarnGlobal _ -> Unit.top ()