Previous  Up  Next

Module Log

module Log: sig .. end

Logging Services for Frama-C Kernel and Plugins.

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;
} 
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.

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

Exception Registry

exception AbortError of string

User error that prevents a plugin to terminate. Argument is the name of the plugin.

exception AbortFatal of string

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

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

module type Messages = sig .. end
val evt_category : event -> string list

Split an event category into its constituants.

val split_category : string -> string list

Split a category specification into its constituants. "*" is considered as empty, and "" categories are skipped.

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

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.

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.

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.

Channel interface

This is the low-level interface to logging services. Not to be used by casual users.

type channel 
val new_channel : string -> channel
val log_channel : channel -> ?kind:kind -> 'a pretty_printer

logging function to user-created channel.

val kernel_channel_name : string

the reserved channel name used by the Frama-C kernel.

val kernel_label_name : string

the reserved label name used by the Frama-C kernel.

val source : file:Filepath.Normalized.t -> line:int -> Filepath.position
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 : Stdlib.Format.formatter
Deprecated.Chlorine-20180501 use Pretty_utils instead.

Prints nothing.

val nullprintf : ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
Deprecated.Chlorine-20180501 use Pretty_utils instead.

Discards the message and returns unit.

val with_null : (unit -> 'b) -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
Deprecated.Chlorine-20180501 use Pretty_utils instead.

Discards the message and call the continuation.

val set_output : ?isatty:bool -> (string -> int -> int -> unit) -> (unit -> unit) -> unit

This function has the same parameters as Format.make_formatter.

val print_on_output : (Stdlib.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.

val print_delayed : (Stdlib.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.