Module State_set

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

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