package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-server.core/Server/Data/index.html

Module `Server.Data`Source

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.

Sourcetype json = Frama_c_kernel.Json.t

Sourceval pretty : Stdlib.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 Jfile : S with type t = Frama_c_kernel.Filepath.t

Sourcemodule Jtext : S with type t = json

Rich text encoding, see Jbuffer.

Sourceval jtext : string -> Jtext.t

Simple string a Jtext

Source

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

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

Sourcemodule Jmarkdown : S with type t = Frama_c_kernel.Markdown.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

Source

val derived : 
  package:Package.package ->
  id:Package.ident ->
  Package.jtype ->
  Package.jtype

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

Source

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

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.

Source

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

Builds an indexer that does not depend on current project.

Source

module 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.

Source

module 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.

Source

module 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.

Source

val failure : 
  ?json:json ->
  ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
  'a

raises InputError
with provided message.

Sourceval failure_from_type_error : string -> json -> 'a

raises InputError
from Yojson.Basic.Util.Type_error arguments.

On This Page

Datatypes
Atomic Data
Constructors
Functional API
Records
Enums
Indexed Values
Error handling

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-server.core/Server/Data/index.html

Module Server.DataSource

Datatypes

Atomic Data

Constructors

Functional API

Records

Enums

Indexed Values

Error handling

Module `Server.Data`Source