Module State_set

module State_set: sig .. end
Functional sets of Cvalue.Model.t, currently implemented as lists without repetition.

type t 
val pretty : Format.formatter -> t -> unit
val empty : t
Creation
val singleton : Cvalue.Model.t * Trace.t -> t
val of_list : (Cvalue.Model.t * Trace.t) list -> t
val of_list_forget_history : Cvalue.Model.t list -> t
val is_empty : t -> bool
Information
val length : t -> int
val add : Cvalue.Model.t * Trace.t -> t -> t
Adding elements
exception Unchanged
val merge_into : t -> into:t -> t
Raise Unchanged if the first set was already included in into
val merge : t -> t -> t
Merge the two sets together. Has a better complexity if the first state has less elements than the second.
val add_statement : t -> Cil_types.stmt -> t
Update the trace of all the states in the stateset.
val fold : ('a -> Cvalue.Model.t * Trace.t -> 'a) -> 'a -> t -> 'a
Iterators
val iter : (Cvalue.Model.t * Trace.t -> unit) -> t -> unit
val exists : (Cvalue.Model.t -> bool) -> t -> bool
val map : (Cvalue.Model.t * Trace.t -> Cvalue.Model.t * Trace.t) ->
t -> t
val reorder : t -> t
Invert the order in which the states are iterated over
val join : t -> Cvalue.Model.t * Trace.t
Export
val to_list : t -> Cvalue.Model.t list