package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/State_selection/index.html

Module `Frama_c_kernel.State_selection`

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

since Carbon-20101201

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Type declarations

type t

Type of a state selection.

since Carbon-20101201

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val only_dependencies : State.t -> t

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

since Carbon-20101201

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

On This Page

Type declarations
Generic Builders
Generic Getters
Specific selections