Frama-C:
Plug-ins:
Libraries:

Frama-C API - Context

Key and structure for abstract contexts. See Structure for more details.

include Structure.Shape with type 'a key = 'a Structure.Key_Context.key and type 'a data = (module Abstract_context.S with type t = 'a)
include Structure.Key with type 'a key = 'a Structure.Key_Context.key
type 'a key = 'a Structure.Key_Context.key
val create_key : string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) Structure.eq option
val name : 'a key -> string
val compare : 'a key -> 'b key -> int
val equal : 'a key -> 'b key -> bool
val hash : 'a key -> int
val tag : 'a key -> int
type 'a data = (module Abstract_context.S with type t = 'a)
type 'a structure =
  1. | Unit : unit structure
  2. | Void : 'a key -> 'a structure
  3. | Leaf : 'a key * 'a data -> 'a structure
  4. | Node : 'a structure * 'b structure -> ('a * 'b) structure
  5. | Option : 'a structure * 'a -> 'a option structure

The gadt, based on keys giving the type of each node. Describes the internal structure of a data type. Used internally to automatically generate efficient accessors of its nodes.

val eq_structure : 'a structure -> 'b structure -> ('a, 'b) Structure.eq option
module type Internal = sig ... end
module type External = sig ... end