Data (p.frama-c.28.0.doc.frama-c-server.core.Server.Data)

frama-c
- README
- Library Pdg_types
  - Pdg_types
- Library frama-c-alias.core
  - Alias
- Library frama-c-aorai.core
  - Aorai
- Library frama-c-api-generator.core
  - Api_generator
- Library frama-c-callgraph.core
  - Callgraph
- Library frama-c-constant_propagation.core
  - Constant_Propagation
- Library frama-c-dive.core
  - Dive
- Library frama-c-e-acsl.core
  - E_ACSL
- Library frama-c-eva.core
  - Eva
- Library frama-c-eva.gui
  - Eva_gui
- Library frama-c-from.core
  - From
- Library frama-c-from.gui
  - From_gui
- Library frama-c-impact.core
  - Impact
- Library frama-c-impact.gui
  - Impact_gui
- Library frama-c-inout.core
  - Inout
- Library frama-c-instantiate.core
  - Instantiate
- Library frama-c-loop-analysis.core
  - LoopAnalysis
- Library frama-c-markdown-report.core
  - Markdown_report
- Library frama-c-markdown-report.eva-info
- Library frama-c-metrics.core
  - Metrics
- Library frama-c-metrics.gui
  - Metrics_gui
- Library frama-c-nonterm.core
  - Nonterm
- Library frama-c-obfuscator.core
  - Obfuscator
- Library frama-c-occurrence.core
  - Occurrence
- Library frama-c-occurrence.gui
  - Occurrence_gui
- Library frama-c-pdg.core
  - Pdg
- Library frama-c-pdg.types
- Library frama-c-postdominators.core
  - Postdominators
- Library frama-c-reduc.core
  - Reduc
- Library frama-c-report.core
  - Report
- Library frama-c-rtegen.core
  - RteGen
- Library frama-c-rtegen.gui
  - Rtegen_gui
- Library frama-c-scope.core
  - Scope
- Library frama-c-scope.gui
  - Scope_gui
- Library frama-c-security_slicing.core
  - Security_slicing
- Library frama-c-security_slicing.gui
  - Security_slicing_gui
- Library frama-c-server.core
  - Server
- Library frama-c-slicing.core
  - Slicing
- Library frama-c-slicing.gui
  - Slicing_gui
- Library frama-c-sparecode.core
  - Sparecode
- Library frama-c-studia.core
  - Studia
- Library frama-c-studia.gui
  - Studia_gui
- Library frama-c-users.core
  - Users
- Library frama-c-variadic.core
  - Variadic
- Library frama-c-wp.core
  - Wp
- Library frama-c-wp.gui
  - Wp_gui
- Library frama-c.analysis-scripts
  - Analysis_scripts
- Library frama-c.boot
  - Frama_c_boot
- Library frama-c.gui
  - Frama_c_gui
- Library frama-c.init
- Library frama-c.kernel
  - Frama_c_kernel
- Library frama_c_very_first_cmdline
- Library frama_c_very_first_gui
- Library markdown_report_eva_info
  - Markdown_report_eva_info
- Library qed
  - Qed
- Sources

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

Sourcemodule Jmarkdown : S with type t = Frama_c_kernel.Markdown.text

Source

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

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

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

raises InputError
with provided message.

Sourceval failure_from_type_error : string -> json -> 'a

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