This section deals with requests related to the management of the Frama-C platform and services offered by the kernel. This covers several topics: configuration, logs.
Configuration deals with versioning and resource directories. Project services allow to work with several Frama-C projects.
Logs are automatically tracked by the server plug-in and
queued. This monitoring can be controlled by
Kernel.SetLogs
command, but by default, monitoring is
turned on as soon as some server is started (except for the batch
server). The Kernel.GetLogs
allow to flush this
queue, with a maximum number of messages. Non-flushed messages can
be recovered by subsequent calls, until the requests replies with
an empty message set.
However, logs emitted prior to the execution of a server, or
after its shutdown, are not collected by default. To
enable this monitoring, for instance to collect messages before
the server is started, you shall set the -server-logs
option, which takes effect at configuration time (you can also use
... -then -server-logs ...
).
GET
)Frama-C Kernel configuration
input
::=
null
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"version" |
string | Frama-C version |
"datadir" |
string
[] |
Shared directory (FRAMAC_SHARE) |
"pluginpath" |
string
[] |
Plugin directories (FRAMAC_PLUGIN) |
SET
)Load a save file. Returns an error, if not successfull.
input
::=
string
output
::=
string?
SET
)Save the current session. Returns an error, if not successfull.
input
::=
string
output
::=
string?
DATA
)Log messages categories.
logkind
::=
tags…
Tags | Value | Description |
---|---|---|
Error | "ERROR" |
User Error |
Warning | "WARNING" |
User Warning |
Feedback | "FEEDBACK" |
Plugin Feedback |
Result | "RESULT" |
Plugin Result |
Failure | "FAILURE" |
Plugin Failure |
Debug | "DEBUG" |
Analyser Debug |
GET
)Registered tags for the above type.
input
::=
null
output
::=
tag
[]
ARRAY
)Log messages
SIGNAL
)Signal for array message
DATA
)Data for array rows message
messageData
::= {
fields…}
Field | Format | Description |
---|---|---|
"key" |
$message |
Entry identifier. |
"kind" |
logkind |
Message kind |
"plugin" |
string | Emitter plugin |
"message" |
string | Message text |
"category" (opt.) |
string | Message category (only for debug or warning messages) |
"source" (opt.) |
source |
Source file position |
"marker" (opt.) |
marker |
Marker at the message position (if any) |
"decl" (opt.) |
decl |
Declaration containing the message position (if any) |
GET
)Data fetcher for array message
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
$message
[] |
removed entries |
"updated" |
messageData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array message
input
::=
null
output
::=
null
DATA
)Message event record.
log
::= {
fields…}
Field | Format | Description |
---|---|---|
"kind" |
logkind |
Message kind |
"plugin" |
string | Emitter plugin |
"message" |
string | Message text |
"category" (opt.) |
string | Message category (DEBUG or WARNING) |
"source" (opt.) |
source |
Source file position |
SET
)Turn logs monitoring on/off
input
::=
boolean
output
::=
null
GET
)Flush the last emitted logs since last call (max 100)
input
::=
null
output
::=
log
[]