Module type Log.Messages

module type Messages = sig .. end
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.

val verbose_atleast : int -> bool
Since Beryllium-20090601-beta1
val debug_atleast : int -> bool
Since Beryllium-20090601-beta1
val printf : ?level:int ->
?dkey:Log.category ->
?current:bool ->
?source:Lexing.position ->
?append:(Format.formatter -> unit) ->
?header:(Format.formatter -> unit) ->
?prefix:string ->
?suffix:string -> ('a, Format.formatter, unit) Pervasives.format -> 'a
Outputs the formatted message on stdout. Levels and key-categories are taken into account like event messages. The header formatted message is emitted as a regular result message. Prefix and suffix strings, if provided, are emitted on stdout as is, at the beginning of an empty line and with a terminal newline character.
val result : ?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer
Results of analysis. Default level is 1.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
val feedback : ?ontty:Log.ontty -> ?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer
Progress and feedback. Level is tested against the verbosity level.
Since Beryllium-20090601-beta1
Change in Fluorine-20130401: Optional parameter ?dkey
Change in Magnesium-20151001: Optional parameter ?ontty
Consult the Plugin Development Guide for additional details.
val debug : ?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer
Debugging information dedicated to Plugin developpers. Default level is 1. The debugging key is used in message headers. See also set_debug_keys and set_debug_keyset.
Since Beryllium-20090601-beta1
Change in Nitrogen-20111001: Optional parameter dkey
Consult the Plugin Development Guide for additional details.
val debug0 : ?level:int -> ?dkey:Log.category -> unit Log.pretty_printer
val debug1 : ?level:int -> ?dkey:Log.category -> ('a -> unit) Log.pretty_printer
val debug2 : ?level:int -> ?dkey:Log.category -> ('a -> 'b -> unit) Log.pretty_printer
val debug3 : ?level:int ->
?dkey:Log.category -> ('a -> 'b -> 'c -> unit) Log.pretty_printer
val debug4 : ?level:int ->
?dkey:Log.category -> ('a -> 'b -> 'c -> 'd -> unit) Log.pretty_printer
val debug5 : ?level:int ->
?dkey:Log.category -> ('a -> 'b -> 'c -> 'd -> 'e -> unit) Log.pretty_printer
val debug6 : ?level:int ->
?dkey:Log.category ->
('a -> 'b -> 'c -> 'd -> 'e -> 'f -> unit) Log.pretty_printer
val debug7 : ?level:int ->
?dkey:Log.category ->
('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> unit) Log.pretty_printer
val debug8 : ?level:int ->
?dkey:Log.category ->
('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> unit) Log.pretty_printer
Specific versions of Log.Messages.debug with fixed arity that are a lot faster than the generic version when debbuging is not activated.
val warning : 'a Log.pretty_printer
Hypothesis and restrictions.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
val error : 'a Log.pretty_printer
user error: syntax/typing error, bad expected input, etc.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.
val abort : ('a, 'b) Log.pretty_aborter
user error stopping the plugin.
Since Beryllium-20090601-beta1
Raises AbortError with the channel name.
Consult the Plugin Development Guide for additional details.
val failure : 'a Log.pretty_printer
internal error of the plug-in.
Consult the Plugin Development Guide for additional details.
val fatal : ('a, 'b) Log.pretty_aborter
internal error of the plug-in.
Since Beryllium-20090601-beta1
Raises AbortFatal with the channel name.
Consult the Plugin Development Guide for additional details.
val verify : bool -> ('a, bool) Log.pretty_aborter
If the first argument is true, return true and do nothing else, otherwise, send the message on the fatal channel and return false.

The intended usage is: assert (verify e "Bla...") ;.
Since Beryllium-20090601-beta1
Consult the Plugin Development Guide for additional details.

val not_yet_implemented : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
raises FeatureRequest but does not send any message. If the exception is not catched, Frama-C displays a feature-request message to the user.
Since Beryllium-20090901
val deprecated : string -> now:string -> ('a -> 'b) -> 'a -> 'b
deprecated s ~now f indicates that the use of f of name s is now deprecated. It should be replaced by now.
Since Beryllium-20090902
Returns the given function itself
val with_result : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
Since Beryllium-20090601-beta1
val with_warning : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
Since Beryllium-20090601-beta1
val with_error : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
Since Beryllium-20090601-beta1
val with_failure : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
Since Beryllium-20090601-beta1
val log : ?kind:Log.kind -> ?verbose:int -> ?debug:int -> 'a Log.pretty_printer
Generic log routine. The default kind is Result. Use cases (with n,m > 0):
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val with_log : (Log.event -> 'b) -> ?kind:Log.kind -> ('a, 'b) Log.pretty_aborter
Since Beryllium-20090901
Consult the Plugin Development Guide for additional details.
val register : Log.kind -> (Log.event -> unit) -> unit
Local registry for listeners.
val register_tag_handlers : (string -> string) * (string -> string) -> unit

Category management


val register_category : string -> Log.category
register a new debugging/verbose category.
Since Fluorine-20130401
val get_category : string -> Log.Category_set.t
returns all registered categories (including sub-categories) corresponding to a given string
Since Fluorine-20130401
val get_all_categories : unit -> Log.Category_set.t
returns all registered categories.
val add_debug_keys : Log.Category_set.t -> unit
adds categories corresponding to string (including potential subcategories) to the set of categories for which messages are to be displayed.
Since Fluorine-20130401 use categories instead of plain string
val del_debug_keys : Log.Category_set.t -> unit
removes the given categories from the set for which messages are printed.
Since Fluorine-20130401
val get_debug_keys : unit -> Log.Category_set.t
Returns currently active keys
Since Fluorine-20130401
val is_debug_key_enabled : Log.category -> bool
Returns true if the given category is currently active
Since Fluorine-20130401
val get_debug_keyset : unit -> Log.category list
Deprecated.Fluorine-20130401 use get_debug_keys instead
Returns currently active keys
Since Nitrogen-20111001