package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Server.DataSource

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.

Sourceval pretty : Format.formatter -> json -> unit
Sourcemodule type S = sig ... end

Datatype module signature.

Atomic Data

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

Rich text encoding, see Jbuffer.

Sourceval jtext : string -> Jtext.t

Simple string a Jtext

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

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

Constructors

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

Functional API

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

Polymorphic data value.

Sourceval junit : unit data
Sourceval jany : json data
Sourceval jbool : bool data
Sourceval jint : int data
Sourceval jfloat : float data
Sourceval jstring : string data
Sourceval jalpha : string data
Sourceval jindex : kind:string -> int data
Sourceval jkey : kind:string -> string data
Sourceval jlist : 'a data -> 'a list data
Sourceval jalist : 'a data -> 'a list data
Sourceval jarray : 'a data -> 'a array data
Sourceval joption : 'a data -> 'a option data
Sourceval data_of_json : 'a data -> json -> 'a
Sourceval data_to_json : 'a data -> 'a -> json

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

Sourceval 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

Sourcemodule Record : sig ... end

Record factory.

Enums

Sourcemodule Tag : S with type t = Package.tagInfo
Sourcemodule 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.
  • Tagged() for projectified values already identified by strings.
Sourcemodule type Info = sig ... end

Datatype registration information.

Sourcemodule type Map = sig ... end

Simplified Map.S.

Sourcemodule type Index = sig ... end

Datatype extended with access to value identifiers.

Sourcemodule Static (M : Map) (_ : Info) : Index with type t = M.key and type tag := int

Builds an indexer that does not depend on current project.

Sourcemodule Index (M : Map) (_ : Info) : Index with type t = M.key and type tag := int

Builds a projectified index.

Sourcemodule type IdentifiedType = sig ... end

Datatype already identified by unique integers.

Sourcemodule Identified (A : IdentifiedType) (_ : Info) : Index with type t = A.t and type tag := int

Builds a projectified index on types with unique identifiers.

Sourcemodule type TaggedType = sig ... end

Datatype already identified by unique integers.

Sourcemodule Tagged (A : TaggedType) (_ : Info) : Index with type t = A.t and type tag := string

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.

Sourceexception InputError of string

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

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

    from Yojson.Basic.Util.Type_error arguments.

OCaml

Innovation. Community. Security.