Frama-C:
Plug-ins:
Libraries:

Frama-C API - Structure

Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes. The leaves must provide a key from a Key module, see key.mli for details.

type (_, _) eq =
  1. | Eq : ('a, 'a) eq

Equality witness between types.

module type Key = sig ... end

Keys identifying datatypes.

module Make () : Key
module Key_Context : Key

Keys module for the abstract contexts of Eva.

module Key_Value : Key

Keys module for the abstract values of Eva.

module Key_Location : Key

Keys module for the abstract locations of Eva.

module Key_Domain : Key

Keys module for the abstract domains of Eva.

module type Shape = sig ... end

A Key module with its structure type.

module Shape (Key : Key) (Data : sig ... end) : Shape with type 'a key = 'a Key.key and type 'a data = 'a Data.t
module type Internal = sig ... end

Internal view of the tree, with the structure.

module type External = sig ... end

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.

module Open (Shape : Shape) (Data : Internal with type 'a structure := 'a Shape.structure) : External with type t := Data.t and type 'a key := 'a Shape.key and type 'a data := 'a Shape.data

Opens an internal tree module into an external one.