Frama-C:
Plug-ins:
Libraries:

Frama-C API - External

External view of the tree, with accessors. Automatically built by the functor Open from an Internal datatype. When a generic datatype is a combination of several other datatypes, these functions allow interacting with its subparts. Note that their behavior is undefined if the overall datatype contains several times the same datatype.

type t
type 'a key
type 'a data
val mem : 'a key -> bool

Tests whether a key belongs to the module.

val get : 'a key -> (t -> 'a) option

For a key of type k key:

  • if the values of type t contain a subpart of type k from a module identified by the key, then get key returns an accessor for it.
  • otherwise, get key returns None.
val set : 'a key -> 'a -> t -> t

For a key of type k key:

  • if the values of type t contain a subpart of type k from a module identified by the key, then set key v t returns the value t in which this subpart has been replaced by v.
  • otherwise, set key _ is the identity function.

Iterators on the components of a structure.

type polymorphic_iter_fun = {
  1. iter : 'a. 'a key -> 'a data -> 'a -> unit;
}
val iter : polymorphic_iter_fun -> t -> unit
type 'b polymorphic_fold_fun = {
  1. fold : 'a. 'a key -> 'a data -> 'a -> 'b -> 'b;
}
val fold : 'b polymorphic_fold_fun -> t -> 'b -> 'b
type polymorphic_map_fun = {
  1. map : 'a. 'a key -> 'a data -> 'a -> 'a;
}
val map : polymorphic_map_fun -> t -> t