Spec.Argmodule Multiplicity : sig ... endmodule D : sig ... endGlobal data is collected using dirty side-effecting.
module V : sig ... endmodule GProtecting : sig ... endCollects information about which variables are protected by which mutexes
module GProtected : sig ... endCollects information about which mutex protects which variable
module G : sig ... endval add :
([ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.t,
'a,
'b,
'c)
Analyses.ctx ->
(Mutexes.elt * bool) ->
[ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.tval remove' :
([ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.t,
'a,
'b,
'c)
Analyses.ctx ->
warn:bool ->
ValueDomain.Addr.t ->
[ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.tval remove :
([ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.t,
'a,
'b,
'c)
Analyses.ctx ->
ValueDomain.Addr.t ->
[ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.tval remove_all :
'a ->
[ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.tval empty :
unit ->
[ `Lifted of BatSet.Make(Lockset.Lock).t | `Top ] * Multiplicity.t