LockDomain.MayLocksetinclude module type of struct include Lockset endmodule RW = Lockset.RWmodule Lock = Lockset.Lockmodule ReverseAddrSet = Lockset.ReverseAddrSetmodule AddrSet = Lockset.AddrSetinclude module type of struct include AddrSet endtype t = Lockset.ReverseAddrSet.tval hash : t -> intval show : t -> stringval pretty : unit -> t -> Goblint_lib__Printable.Pretty.docval to_yojson : t -> Yojson.Safe.tval tag : t -> intval widen :
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.tval narrow :
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.tval is_bot : Lockset.ReverseAddrSet.t -> boolval is_top : Lockset.ReverseAddrSet.t -> boolval printXml : 'a BatInnerIO.output -> Lockset.ReverseAddrSet.t -> unitval arbitrary : unit -> Lockset.ReverseAddrSet.t QCheck.arbitraryval add : (Addr.t * RW.t) -> ReverseAddrSet.t -> ReverseAddrSet.tval remove : (Addr.t * RW.t) -> ReverseAddrSet.t -> ReverseAddrSet.tval empty : unit -> ReverseAddrSet.tval is_empty : ReverseAddrSet.t -> boolval filter :
(ReverseAddrSet.elt -> bool) ->
ReverseAddrSet.t ->
ReverseAddrSet.tval fold : (ReverseAddrSet.elt -> 'a -> 'a) -> ReverseAddrSet.t -> 'a -> 'aval singleton : ReverseAddrSet.elt -> ReverseAddrSet.tval mem : ReverseAddrSet.elt -> ReverseAddrSet.t -> boolval exists : (ReverseAddrSet.elt -> bool) -> ReverseAddrSet.t -> boolval export_locks : ReverseAddrSet.t -> Mutexes.tval leq : ReverseAddrSet.t -> ReverseAddrSet.t -> boolval join :
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.tval meet :
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.t ->
Lockset.ReverseAddrSet.tval top : unit -> Lockset.ReverseAddrSet.tval bot : unit -> Lockset.ReverseAddrSet.t