Frama-C:
Plug-ins:
Libraries:

Frama-C API - Shape

include Key
type 'a key
val create_key : string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) 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
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) eq option