Frama_c_kernel.State_selection
A state selection is a set of states with operations for easy handling of state dependencies.
val empty : t
The empty selection.
val full : t
The selection containing all the states.
val is_empty : t -> bool
val is_full : t -> bool
The selection containing the given state and all its dependencies.
The selection containing all the dependencies of the given state (but not this state itself).
The selection containing the given state and all its co-dependencies.
The selection containing all the co-dependencies of the given state (but not this state itself).
val cardinal : t -> int
Size of a selection.
val pretty : Stdlib.Format.formatter -> t -> unit
Display a selection.
val pretty_witness : Stdlib.Format.formatter -> t -> unit
Display a selection in a more concise form. (Using the atomic operations that were used to create it.)
Iterate over the successor of a state in a selection. The order is unspecified.
Iterate over the successor of a state in a selection. The order is unspecified.
Iterate over a selection in a topological ordering compliant with the State Dependency Graph. Less efficient that iter
.