Spec.Amodule RW = IntDomain.Booleansmodule Lock : sig ... endmodule ReverseAddrSet : sig ... endmodule AddrSet : sig ... endtype t = 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 : ReverseAddrSet.t -> ReverseAddrSet.t -> ReverseAddrSet.tval narrow : ReverseAddrSet.t -> ReverseAddrSet.t -> ReverseAddrSet.tval bot : unit -> ReverseAddrSet.tval is_bot : ReverseAddrSet.t -> boolval top : unit -> ReverseAddrSet.tval is_top : ReverseAddrSet.t -> boolval leq : ReverseAddrSet.t -> ReverseAddrSet.t -> boolval join : ReverseAddrSet.t -> ReverseAddrSet.t -> ReverseAddrSet.tval meet : ReverseAddrSet.t -> ReverseAddrSet.t -> ReverseAddrSet.tval printXml : 'a BatInnerIO.output -> ReverseAddrSet.t -> unitval arbitrary : unit -> ReverseAddrSet.t QCheck.arbitraryval may_be_same_offset :
([> `Field of GoblintCil.fieldinfo * 'a
| `Index of Goblint_lib.ValueDomain.IndexDomain.t * 'a
| `NoOffset ] as 'a) ->
([> `Field of GoblintCil.fieldinfo * 'b
| `Index of Goblint_lib.ValueDomain.IndexDomain.t * 'b
| `NoOffset ] as 'b) ->
boolval add :
(Goblint_lib.ValueDomain.Addr.t * RW.t) ->
ReverseAddrSet.t ->
ReverseAddrSet.tval remove :
(Goblint_lib.ValueDomain.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 ->
[ `Lifted of BatSet.Make(Goblint_lib.ValueDomain.Addr).t | `Top ]val may_race : D.ReverseAddrSet.t -> D.ReverseAddrSet.t -> boolval should_print : ReverseAddrSet.t -> bool