package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Data Encoding.

Datatypes

This module is responsible for marshaling and demarshaling data to handle communications between the server and the client in both directions.

Each datatype must be equipped with functions to encode and decode values to/from JSON format. Moreover, data types shall be also properly documented and registered in the generated documentation of the Frama-C server.

Generally speaking, we will have a module with signature Data.D for every datatype to be exchanged with the server. For simple values, predefined modules are already provided. More complex datatypes can be built with some functors, typically for options, lists or arrays.

Records and enumerated types are typical in JSON formatting, but difficult to build from OCaml records and abstract datatypes. For those kinds of data, we provide an API based on the following general scheme:

  • First create an empty container with its name, documentation and such;
  • Then add each field or constructor to the container;
  • Finally pack the container, which actually registers its complete documentation and returns an OCaml value containing the resulting datatype module.

Hence, in addition to module signature Data.S for values, there is also a polymorphic type 'a Data.data for module values carrying a data module with type t = 'a.

The same mechanism is used throughout modules States and Request each time a JSON record or tag is needed.

val pretty : Format.formatter -> json -> unit
module type S = sig ... end

Datatype module signature.

Atomic Data

module Junit : S with type t = unit
module Jany : S with type t = json
module Jbool : S with type t = bool
module Jint : S with type t = int
module Jfloat : S with type t = float
module Jstring : S with type t = string
module Jalpha : S with type t = string
module Jtext : S with type t = json

Rich text encoding, see Jbuffer.

val jpretty : ?indent:int -> ?margin:int -> (Format.formatter -> 'a -> unit) -> 'a -> Jtext.t

All-in-one formatter. Return the JSON encoding of formatted text.

Constructors

module Joption (A : S) : S with type t = A.t option
module Jpair (A : S) (B : S) : S with type t = A.t * B.t
module Jtriple (A : S) (B : S) (C : S) : S with type t = A.t * B.t * C.t
module Jlist (A : S) : S with type t = A.t list
module Jarray (A : S) : S with type t = A.t array

Functional API

type 'a data = (module S with type t = 'a)

Polymorphic data value.

val junit : unit data
val jany : json data
val jbool : bool data
val jint : int data
val jfloat : float data
val jstring : string data
val jalpha : string data
val jindex : kind:string -> int data
val jkey : kind:string -> string data
val jlist : 'a data -> 'a list data
val jalist : 'a data -> 'a list data
val jarray : 'a data -> 'a array data
val joption : 'a data -> 'a option data
val derived : package:Package.package -> id:Package.ident -> Package.jtype -> unit

Declare the derived names for the provided type. Shall not be used directely.

val declare : package:Package.package -> name:string -> ?descr:Frama_c_kernel.Markdown.text -> Package.jtype -> Package.jtype

Declare a new type and returns its alias. Same as Jdata (declare_id ~package ~name (D_type js)). Automatically declare the derived names.

Records

module Record : sig ... end

Record factory.

Enums

module Tag : S with type t = Package.tagInfo
module Enum : sig ... end

Enum factory.

Indexed Values

These datatypes automatically index complex values with unique identifiers. This avoids to encode the internal OCaml representation of each value, by only providing to the server a unique identifier for each value.

These datatype functors come into three flavors:

  • Index() for projectified datatypes,
  • Static() for project independant datatypes,
  • Identified() for projectified values already identified by integers.
module type Info = sig ... end

Datatype information.

module type Map = sig ... end

Simplified Map.S.

module type Index = sig ... end

Datatype extended with access to value identifiers.

module Static (M : Map) (I : Info) : Index with type t = M.key

Builds an indexer that does not depend on current project.

module Index (M : Map) (I : Info) : Index with type t = M.key

Builds a projectified index.

module type IdentifiedType = sig ... end

Datatype already identified by unique integers.

module Identified (A : IdentifiedType) (I : Info) : Index with type t = A.t

Builds a projectified index on types with unique identifiers.

Error handling

These utilities shall be used when writing your own encoding and decoding values to JSON format.

exception InputError of string

Exception thrown during the decoding of a request's inputs.

val failure : ?json:json -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val failure_from_type_error : string -> json -> 'a
  • raises InputError

    from Yojson.Basic.Util.Type_error arguments.