Module `ConcDomain.MustThreadSet`

type elt = ThreadSet.elt

val empty : unit -> ThreadSet.t

val is_empty : ThreadSet.t -> bool

val mem : elt -> ThreadSet.t -> bool

val add : elt -> ThreadSet.t -> ThreadSet.t

val singleton : elt -> ThreadSet.t

val remove : elt -> ThreadSet.t -> ThreadSet.t

val union : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val inter : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val diff : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val subset : ThreadSet.t -> ThreadSet.t -> bool

val iter : (elt -> unit) -> ThreadSet.t -> unit

val map : (elt -> elt) -> ThreadSet.t -> ThreadSet.t

val fold : (elt -> 'a -> 'a) -> ThreadSet.t -> 'a -> 'a

val for_all : (elt -> bool) -> ThreadSet.t -> bool

val exists : (elt -> bool) -> ThreadSet.t -> bool

val filter : (elt -> bool) -> ThreadSet.t -> ThreadSet.t

val partition : (elt -> bool) -> ThreadSet.t -> ThreadSet.t * ThreadSet.t

val cardinal : ThreadSet.t -> int

val elements : ThreadSet.t -> elt list

val of_list : elt list -> ThreadSet.t

val min_elt : ThreadSet.t -> elt

val max_elt : ThreadSet.t -> elt

val choose : ThreadSet.t -> elt

val split : elt -> ThreadSet.t -> ThreadSet.t * bool * ThreadSet.t

type t = ThreadSet.t

val equal : t -> t -> bool

val hash : t -> int

val compare : t -> t -> int

val show : t -> string

val pretty : unit -> t -> Pretty.doc

val to_yojson : t -> Printable.json

val invariant : Invariant.context -> t -> Invariant.t

val tag : t -> int

val relift : t -> t

val widen : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val narrow : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val bot : unit -> ThreadSet.t

val is_bot : ThreadSet.t -> bool

val top : unit -> ThreadSet.t

val is_top : ThreadSet.t -> bool

val leq : ThreadSet.t -> ThreadSet.t -> bool

val join : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val meet : ThreadSet.t -> ThreadSet.t -> ThreadSet.t

val name : unit -> string

val pretty_diff : unit -> (t * t) -> Pretty.doc

val printXml : 'a BatInnerIO.output -> ThreadSet.t -> unit

val arbitrary : unit -> ThreadSet.t QCheck.arbitrary

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ConcDomain/MustThreadSet/index.html

Module `ConcDomain.MustThreadSet`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ConcDomain/MustThreadSet/index.html

Module ConcDomain.MustThreadSet

Module `ConcDomain.MustThreadSet`