Module Log

module Log: sig .. end
Logging Services for Frama-C Kernel and Plugins.
Since Beryllium-20090601-beta1

type kind = 
| Result
| Feedback
| Debug
| Warning
| Error
| Failure
type event = {
   evt_kind : kind;
   evt_plugin : string;
   evt_category : string option; (*
message or warning category
*)
   evt_source : Filepath.position option;
   evt_message : string;
}
Since Beryllium-20090601-beta1
type 'a pretty_printer = ?current:bool ->
?source:Filepath.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.
Since Beryllium-20090601-beta1
type ('a, 'b) pretty_aborter = ?current:bool ->
?source:Filepath.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
User error that prevents a plugin to terminate. Argument is the name of the plugin.
Since Beryllium-20090601-beta1
exception AbortFatal of string
Internal error that prevents a plugin to terminate. Argument is the name of the plugin.
Since Beryllium-20090601-beta1
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 ontty = [ `Feedback | `Message | `Silent | `Transient ] 
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
Since Chlorine-20180501
module type Messages = sig .. end
val evt_category : event -> string list
Split an event category into its constituants.
Since 18.0-Argon
val split_category : string -> string list
Split a category specification into its constituants. "*" is considered as empty, and "" categories are skipped.
Since 18.0-Argon
val is_subcategory : string list -> string list -> bool
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).
Since 18.0-Argon
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
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val log_channel : channel -> ?kind:kind -> 'a pretty_printer
logging function to user-created channel.
Since Beryllium-20090901
Change in Chlorine-20180501: removed ~prefix
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 source : file:Filepath.Normalized.t -> line:int -> Filepath.position
Since Chlorine-20180501
Change in 18.0-Argon: change type of file
val get_current_source : unit -> Filepath.position

Terminal interface

This is the low-level interface to logging services. Not to be used by casual users.
val clean : unit -> unit
Flushes the last transient message if necessary.
val null : Format.formatter
Deprecated.Chlorine-20180501 use Pretty_utils instead.
Prints nothing.
Since Beryllium-20090901
val nullprintf : ('a, Format.formatter, unit) Pervasives.format -> 'a
Deprecated.Chlorine-20180501 use Pretty_utils instead.
Discards the message and returns unit.
Since Beryllium-20090901
val with_null : (unit -> 'b) -> ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
Deprecated.Chlorine-20180501 use Pretty_utils instead.
Discards the message and call the continuation.
Since Beryllium-20090901
val set_output : ?isatty:bool -> (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.