package frama-c

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

Module Server.MainSource

Server Main Process

Sourcetype kind = [
  1. | `GET
  2. | `SET
  3. | `EXEC
]
Sourceval string_of_kind : kind -> string
Sourceval pp_kind : Format.formatter -> kind -> unit

Request Registry

Sourceval register : kind -> string -> (json -> json) -> unit
Sourceval find : string -> (kind * (json -> json)) option
Sourceval exec : string -> json -> json

Signals Registry

Sourcetype signal
Sourceval signal : string -> signal
Sourceval signal_name : signal -> string

Server Main Process

Sourcetype 'a request = [
  1. | `Poll
  2. | `Request of 'a * string * json
  3. | `Kill of 'a
  4. | `SigOn of string
  5. | `SigOff of string
  6. | `Shutdown
]

Type of request messages. Parametrized by the type of request identifiers.

Sourcetype 'a response = [
  1. | `Data of 'a * json
  2. | `Error of 'a * string
  3. | `Killed of 'a
  4. | `Rejected of 'a
  5. | `Signal of string
  6. | `CmdLineOn
  7. | `CmdLineOff
]

Type of response messages. Parametrized by the type of request identifiers.

Sourcetype 'a message = {
  1. requests : 'a request list;
  2. callback : 'a response list -> unit;
}

A paired request-response message. The callback will be called exactly once for each received message.

Sourcetype 'a server
Sourceval create : pretty:(Format.formatter -> 'a -> unit) -> ?equal:('a -> 'a -> bool) -> fetch:(unit -> 'a message option) -> unit -> 'a server

Run a server with the provided low-level network primitives to actually exchange data. Logs are monitored unless ~logs:false is specified.

Default equality is the standard `(=)` one.

Sourceval start : 'a server -> unit

Start the server in background.

The function returns immediately after installing a daemon that (only) accepts GET requests received by the server on calls to Async.yield().

Shall be scheduled at command line main stage via Boot.Main.extend extension point.

Sourceval stop : 'a server -> unit

Stop the server if it is running in background.

Can be invoked to force server shutdown at any time.

It shall be typically scheduled via Extlib.safe_at_exit along with other system cleanup operations to make sure the server is property shutdown before Frama-C main process exits.

Sourceval run : 'a server -> unit

Run the server forever. The server would now accept any kind of requests and start handling them. While executing an `EXEC request, the server would continue to handle (only) `GET pending requests on Async.yield() at every server.polling time interval.

The function will not return until the server is actually shutdown.

Shall be scheduled at normal command line termination via Cmdline.at_normal_exit extension point.

Sourceval kill : unit -> 'a

Kill the currently running request by raising an exception.

Sourceval emit : signal -> unit

Emit the server signal to the client.

Sourceval on_signal : signal -> (bool -> unit) -> unit

Register a callback on signal listening.

The callback is invoked with true on SIGON command and false on SIGOFF.

Sourceval on : (bool -> unit) -> unit

Register a callback to listen for server activity. All callbacks are executed in their order of registration. Callbacks shall never raise any exception.

Sourceval once : (unit -> unit) -> unit

Register a callback to listen for server initialization. All callbacks are executed once, in their order of registration, and before activity callbacks. Callbacks shall never raise any exception.

Sourceval async : ('a -> 'b) -> 'a -> 'b Frama_c_kernel.Task.task

Register an asynchronous task on the server. When the server is not working in background, this is equivalent to Task.call ; otherwize, the continuation is scheduled on the server like an `EXEC request.

OCaml

Innovation. Community. Security.