Module Server.Main

module Main: sig .. end

Server Main Process

type json = Json.t

type kind = [ `EXEC | `GET | `SET ]

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

Signals Registry

type signal

val signal : string -> signal

val signal_name : signal -> string

Server Main Process

type 'a request = [ `Kill of 'a
       | `Poll
       | `Request of 'a * string * json
       | `Shutdown
       | `SigOff of string
       | `SigOn of string ]

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

type 'a response = [ `CmdLineOff
       | `CmdLineOn
       | `Data of 'a * json
       | `Error of 'a * string
       | `Killed of 'a
       | `Rejected of 'a
       | `Signal of string ]

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

type 'a message = {

	`requests : 'a request list;`
	`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 Db.yield().

Shall be scheduled at command line main stage via Db.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 Db.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

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.