Frama-C:
Plug-ins:
Libraries:

Frama-C API - External

include Internal
include Abstract_context.S
type t
val top : t

The default context used in a top abstract state, or if no domain has been enabled — or no domain providing this context.

val narrow : t -> t -> t Eval.or_bottom

In a product of abstract domains, merges the context provided by the abstract state of each domain.

val structure : t structure
include Structure.External with type t := t and type 'a key := 'a key and type 'a data := '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