Frama_c_kernel.Log
Logging Services for Frama-C Kernel and Plugins.
type event = {
evt_kind : kind;
evt_plugin : string;
evt_category : string option;
message or warning category
*)evt_source : Filepath.position option;
evt_message : string;
}
type 'a pretty_printer =
?current:bool ->
?source:Filepath.position ->
?emitwith:(event -> unit) ->
?echo:bool ->
?once:bool ->
?append:(Stdlib.Format.formatter -> unit) ->
('a, Stdlib.Format.formatter, unit) Stdlib.format ->
'a
Generic type for the various logging channels which are not aborting Frama-C. The first line will be prefixed (plugin name, location, message kind, etc.), consider skipping the first line (by adding a new line) if you want to keep the message alignment on multi-lines messages.
current
is false
(default for most of the channels), no location is output. When it is true
, the last registered location is used as current (see Current_loc
).source
is the location to be output. If nil, current
is used to determine if a location should be outputemitwith
function which is called each time an event is processedecho
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.type ('a, 'b) pretty_aborter =
?current:bool ->
?source:Filepath.position ->
?echo:bool ->
?append:(Stdlib.Format.formatter -> unit) ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 ->
'a
Same as Log.pretty_printer
except that channels having this type denote a fatal error aborting Frama-C.
User error that prevents a plugin to terminate. Argument is the name of the plugin.
Internal error that prevents a plugin to terminate. Argument is the name of the plugin.
exception FeatureRequest of Filepath.position option * string * string
Raised by not_yet_implemented
. You may catch FeatureRequest(s,p,r)
to support degenerated behavior. The (optional) source location is s, the responsible plugin is 'p' and the feature request is 'r'.
type warn_status =
| Winactive
nothing is emitted.
*)| Wfeedback_once
combines feedback and once.
*)| Wfeedback
emit a feedback message.
*)| Wonce
emit a warning message, but only the first time the category is encountered.
*)| Wactive
emit a warning message.
*)| Werror_once
combines once and error.
*)| Werror
emit a message. Execution continues, but exit status will not be 0
*)| Wabort
emit a message and abort execution
*)status of a warning category
module type Messages = sig ... end
val evt_category : event -> string list
Split an event category into its constituants.
Split a category specification into its constituants. "*"
is considered as empty, and ""
categories are skipped.
Sub-category checks. is_subcategory a b
checks whether a
is a sub-category of b
. Indeed, it checks whether b
is a prefix of a
, that is, that a
equals b
or refines b
with (a list of) sub-category(ies).
Each plugin has its own channel to output messages. This functor should not be directly applied by plug-in developer. They should apply Plugin.Register
instead.
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.
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.
Warning: when executing the listener, all listeners will be temporarily deactivated in order to avoid infinite recursion.
val echo : event -> unit
Display an event of the terminal, unless echo has been turned off.
val notify : event -> unit
Send an event over the associated listeners.
This is the low-level interface to logging services. Not to be used by casual users.
val new_channel : string -> channel
val log_channel : channel -> ?kind:kind -> 'a pretty_printer
logging function to user-created channel.
val source : file:Filepath.t -> line:int -> Filepath.position
val get_current_source : unit -> Filepath.position
This is the low-level interface to logging services. Not to be used by casual users.
This function has the same parameters as Format.make_formatter.
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.
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.