package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

A state selection is a set of states with operations for easy handling of state dependencies.

  • since Carbon-20101201

Type declarations

type t

Type of a state selection.

  • since Carbon-20101201
val ty : t Type.t

Type value representing t.

  • since Carbon-20101201

Generic Builders

val empty : t

The empty selection.

  • since Carbon-20101201
val full : t

The selection containing all the states.

  • since Carbon-20101201
val singleton : State.t -> t

The selection containing only the given state.

  • since Carbon-20101201
val of_list : State.t list -> t

The selection containing only the given list of states.

  • since Carbon-20101201

Generic Getters

val is_empty : t -> bool
  • returns

    true iff the selection is empty.

  • since Carbon-20101201
val is_full : t -> bool
  • returns

    true iff the selection contains all the states.

  • since Carbon-20101201
val mem : t -> State.t -> bool

Specific selections

Builders from dependencies

val with_dependencies : State.t -> t

The selection containing the given state and all its dependencies.

  • since Carbon-20101201
val only_dependencies : State.t -> t

The selection containing all the dependencies of the given state (but not this state itself).

  • since Carbon-20101201
val with_codependencies : State.t -> t

The selection containing the given state and all its co-dependencies.

  • since Carbon-20101201
val only_codependencies : State.t -> t

The selection containing all the co-dependencies of the given state (but not this state itself).

  • since Carbon-20101201

Builders by operations over sets

val union : t -> t -> t

Union of two selections.

  • since Carbon-20101201
val list_union : t list -> t

Union of an arbitrary number of selection (0 gives an empty selection)

  • since Oxygen-20120901
val diff : t -> t -> t

Difference between two selections.

  • since Carbon-20101201

Specific Getters

val cardinal : t -> int

Size of a selection.

  • since Carbon-20101201
val to_list : t -> State.t list

Convert a selection into a list of states.

  • since Fluorine-20130401
val pretty : Format.formatter -> t -> unit

Display a selection.

  • since Carbon-20101201
val pretty_witness : Format.formatter -> t -> unit

Display a selection in a more concise form. (Using the atomic operations that were used to create it.)

  • since Aluminium-20160501

Iterators

val iter_succ : (State.t -> unit) -> t -> State.t -> unit

Iterate over the successor of a state in a selection. The order is unspecified.

  • since Carbon-20101201
val fold_succ : (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a

Iterate over the successor of a state in a selection. The order is unspecified.

  • since Carbon-20101201
val iter : (State.t -> unit) -> t -> unit

Iterate over a selection. The order is unspecified.

  • since Carbon-20101201
val fold : (State.t -> 'a -> 'a) -> t -> 'a -> 'a

Fold over a selection. The order is unspecified.

  • since Carbon-20101201
val iter_in_order : (State.t -> unit) -> t -> unit

Iterate over a selection in a topological ordering compliant with the State Dependency Graph. Less efficient that iter.

  • since Carbon-20101201
val fold_in_order : (State.t -> 'a -> 'a) -> t -> 'a -> 'a

Fold over a selection in a topological ordering compliant with the State Dependency Graph. Less efficient that iter.

  • since Carbon-20101201
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct