Module Log
module Log: sig
.. end
Logging Services for Frama-C Kernel and Plugins.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
type
kind =
| |
Result |
| |
Feedback |
| |
Debug |
| |
Warning |
| |
Error |
| |
Failure |
type
event = {
|
evt_kind : kind ; |
|
evt_plugin : string ; |
|
evt_source : Lexing.position option ; |
|
evt_message : string ; |
}
Since Beryllium-20090601-beta1
type 'a
pretty_printer = ?current:bool ->
?source:Lexing.position ->
?emitwith:(event -> unit) ->
?echo:bool ->
?once:bool ->
?append:(Format.formatter -> unit) ->
('a, Format.formatter, unit) Pervasives.format -> 'a
Generic type for the various logging channels which are not aborting
Frama-C.
- When
current
is false
(default for most of the channels),
no location is output. When it is true
, the last registred location
is used as current (see Cil_const.CurrentLoc
).
source
is the location to be output. If nil, current
is used to
determine if a location should be output
emitwith
function which is called each time an event is processed
echo
is true
if the event should be output somewhere in addition
to stdout
append
adds some actions performed on the formatter after the event
has been processed.
Since Beryllium-20090601-beta1
type ('a, 'b)
pretty_aborter = ?current:bool ->
?source:Lexing.position ->
?echo:bool ->
?append:(Format.formatter -> unit) ->
('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
Since Beryllium-20090601-beta1
Same as {!Log.pretty_printer} except that channels having this type
denote a fatal error aborting Frama-C.
Exception Registry
exception AbortError of string
Plug-in name
User error that prevents a plugin to terminate.
exception AbortFatal of string
Plug-in name
Internal error that prevents a plugin to terminate.
exception FeatureRequest of string * string
Raised by not_yet_implemented
.
You may catch FeatureRequest(p,r)
to support degenerated behavior.
The responsible plugin is 'p' and the feature request is 'r'.
Option_signature.Interface
type
category = private string
category for debugging/verbose messages. Must be registered before
any use.
Each column in the string defines a sub-category, e.g.
a:b:c defines a subcategory c of b, which is itself a subcategory of a.
Enabling a category (via -plugin-msg-category) will enable all its
subcategories.
Since Fluorine-20130401
module Category_set: FCSet.S
with type elt = category
sets of category keywords
module type Messages = sig
.. end
module Register: functor (
P
:
sig
val channel : string
val label : string
val verbose_atleast : int -> bool
val debug_atleast : int -> bool
end
) ->
Messages
Each plugin has its own channel to output messages.
Echo and Notification
val set_echo : ?plugin:string -> ?kind:kind list -> bool -> unit
Turns echo on or off. Applies to all channel unless specified,
and all kind of messages unless specified.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
val add_listener : ?plugin:string -> ?kind:kind list -> (event -> unit) -> unit
Register a hook that is called each time an event is
emitted. Applies to all channel unless specified,
and all kind of messages unless specified.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
val echo : event -> unit
Display an event of the terminal, unless echo has been turned off.
Since Beryllium-20090601-beta1
val notify : event -> unit
Send an event over the associated listeners.
Since Beryllium-20090601-beta1
Channel interface
This is the low-level interface to logging services.
Not to be used by casual users.
type
channel
Since Beryllium-20090601-beta1
val new_channel : string -> channel
type
prefix =
| |
Label of string |
| |
Prefix of string |
| |
Indent of int |
val log_channel : channel -> ?kind:kind -> ?prefix:prefix -> 'a pretty_printer
logging function to user-created channel.
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val with_log_channel : channel ->
(event -> 'b) ->
?kind:kind -> ?prefix:prefix -> ('a, 'b) pretty_aborter
logging function to user-created channel.
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val kernel_channel_name : string
the reserved channel name used by the Frama-C kernel.
Since Beryllium-20090601-beta1
val kernel_label_name : string
the reserved label name used by the Frama-C kernel.
Since Beryllium-20090601-beta1
val get_current_source : unit -> Lexing.position
Terminal interface
This is the low-level interface to logging services.
Not to be used by casual users.
val null : Format.formatter
Prints nothing.
Since Beryllium-20090901
val nullprintf : ('a, Format.formatter, unit) Pervasives.format -> 'a
Discards the message and returns unit.
Since Beryllium-20090901
val with_null : (unit -> 'b) -> ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
Discards the message and call the continuation.
Since Beryllium-20090901
val set_output : (string -> int -> int -> unit) -> (unit -> unit) -> unit
This function has the same parameters as Format.make_formatter.
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val print_on_output : (Format.formatter -> unit) -> unit
Direct printing on output.
Message echo is delayed until the output is finished.
Then, the output is flushed and all pending message are echoed.
Notification of listeners is not delayed, however.
Can not be recursively invoked.
Since Beryllium-20090901
Change in Nitrogen-20111001: signature changed
Consult the Plugin Development Guide for additional details.
val print_delayed : (Format.formatter -> unit) -> unit
Direct printing on output. Same as
print_on_output
, except
that message echo is not delayed until text material is actually
written. This gives an chance for formatters to emit messages
before actual pretty printing.
Can not be recursively invoked.
Since Beryllium-20090901
Change in Nitrogen-20111001: signature changed
Consult the Plugin Development Guide for additional details.