Frama-C:
Plug-ins:
Libraries:

Frama-C API - Main

Server Main Process

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

Request Registry

val register : kind -> string -> (json -> json) -> unit
val find : string -> (kind * (json -> json)) option
val exec : string -> json -> json
  • raises Not_found

    if not registered.

Signals Registry

type signal
val signal : string -> signal
val signal_name : signal -> string

Server Main Process

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

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

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

type 'a server
val create : pretty:(Stdlib.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.

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

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

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

val kill : unit -> 'a

Kill the currently running request by raising an exception.

val emit : signal -> unit

Emit the server signal to the client.

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

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

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

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