Kernel Services

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

kernel.services.getConfig (GET)

Frama-C Kernel configuration

input ::= null

output ::= { output… }

Output Format Description
"version" string Frama-C version
"codename" string Frama-C codename
"version_codename" string Frama-C version and codename
"datadir" string [] Shared directory (FRAMAC_SHARE)
"pluginpath" string [] Plugin directories (FRAMAC_PLUGIN)

kernel.services.load (SET)

Load a save file. Returns an error, if not successfull.

input ::= string

output ::= string ?

kernel.services.save (SET)

Save the current session. Returns an error, if not successfull.

input ::= string

output ::= string ?

kernel.services.logkind (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

kernel.services.logkindTags (GET)

Registered tags for the above type.

input ::= null

output ::= tag []

kernel.services.message (ARRAY)

Log messages

kernel.services.signalMessage (SIGNAL)

Signal for array message

kernel.services.messageData (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)

kernel.services.fetchMessage (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

kernel.services.reloadMessage (GET)

Force full reload for array message

input ::= null

output ::= null

kernel.services.log (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

kernel.services.setLogs (SET)

Turn logs monitoring on/off

input ::= boolean

output ::= null

kernel.services.getLogs (GET)

Flush the last emitted logs since last call (max 100)

input ::= null

output ::= log []