This section presents a ZeroMQ
based entry point for Frama-C Server. It is activated by option
-server-zmq <URL>
option of the Server plug-in,
which is compiled when the OCaml package zmq
is
detected at Frama-C configure time.
The protocol builds a ZeroMQ socket of type REP
which is the standard for a request server. It is meant for
accepting connection from a ZeroMQ socket of type REQ
on the same URL
. The paired
REP
-REQ
sockets use ZeroMQ
multi-part messages to transfer data.
A typical example to start a Frama-C server for inter-process communication is:
$ frama-c [options...] -then -server-zmq ipc:///tmp/my-server.io
Each input message consists of a list of commands. Each command takes a fixed number of parts from the incomming ZeroMQ message. The first part of each command is a single string identifying the command:
Commands | Parts | Part 1 | Part 2 | Part 3 | Part 4 |
---|---|---|---|---|---|
POLL() |
1 | "POLL" |
|||
GET(id,request,data) |
4 | "GET" |
id | request | data |
SET(id,request,data) |
4 | "SET" |
id | request | data |
EXEC(id,request,data) |
4 | "EXEC" |
id | request | data |
SIGON(id) |
2 | "SIGON" |
id | ||
SIGOFF(id) |
2 | "SIGOFF" |
id | ||
KILL(id) |
2 | "KILL" |
id | ||
SHUTDOWN |
1 | "SHUTDOWN" |
Each output message consists of a list of replies. Each reply takes a fixed number of parts from the incomming ZeroMQ message. The first part of each reply is a finel string identifying the reply:
Replies | Parts | Part 1 | Part 2 | Part 3 |
---|---|---|---|---|
DATA(id,data) |
3 | "DATA" |
id | data |
ERROR(id,message) |
4 | "ERROR" |
id | message |
KILLED(id) |
2 | "KILLED" |
id | |
REJECTED(id) |
2 | "REJECTED" |
id | |
SIGNAL(id) |
2 | "SIGNAL" |
id | |
CMDLINEON |
1 | "CMDLINEON" |
||
CMDLINEOFF |
1 | "CMDLINEOFF" |
||
(special) | 2 | "WRONG" |
message | |
(special) | 1 | "NONE" |
The two special responses "WRONG"
and
"NONE"
are used to handle special issues with the
ZeroMQ layer protocol: WRONG(message)
signals an
error in the message formats; NONE
is used in the
special case where the reply message from the server is completely
empty. This generaly means that the server is busy or idled.
Request identifiers can be any string, encoded into a single part of a ZeroMQ message.
Data are stringified JSON data structures. Each command or reply data shall be packed into a single JSON data, which leads to a single part of the associated ZeroMQ message.
Since ZeroMQ prococol accepts any kind of strings as a single message part, the stringified JSON data might contains spaces, newlines and any other spacing characters.