Module type Log.Messages

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

type category 
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
Change in Chlorine-20180501: categories are an abstract type of each plug-in
type warn_category 
Same as above, but for warnings
Since Chlorine-20180501
val verbose_atleast : int -> bool
Since Beryllium-20090601-beta1
val debug_atleast : int -> bool
Since Beryllium-20090601-beta1
val printf : ?level:int ->
?dkey:category ->
?current:bool ->
?source:Filepath.position ->
?append:(Format.formatter -> unit) ->
?header:(Format.formatter -> unit) ->
('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.
val result : ?level:int -> ?dkey: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: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:category -> 'a Log.pretty_printer
Debugging information dedicated to Plugin developers. 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 warning : ?wkey:warn_category -> '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 caught, 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 option -> 'b) -> ('a, 'b) Log.pretty_aborter
with_result f fmt calls f in the same condition as logwith.
Since Beryllium-20090601-beta1
val with_warning : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter
with_warning f fmt calls f in the same condition as logwith.
Since Beryllium-20090601-beta1
val with_error : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter
with_error f fmt calls f in the same condition as logwith.
Since Beryllium-20090601-beta1
val with_failure : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter
with_failure f fmt calls f in the same condition as logwith.
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 logwith : (Log.event option -> 'b) ->
?wkey:warn_category ->
?emitwith:(Log.event -> unit) -> ?once:bool -> ('a, 'b) Log.pretty_aborter
Recommanded generic log routine using warn_category instead of kind. logwith continuation ?wkey fmt similar to warning ?wkey fmt and then calling the continuation. The optional continuation argument refers to the corresponding event. None is used iff no message is logged. In case the wkey is considered as a Failure, the continution is not called. This kind of message denotes a fatal error aborting Frama-C. Notice that the ~emitwith action is called iff a message is logged.
Since 18.0-Argon
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 -> category
register a new debugging/verbose category. Note: categories must be added (e.g. via add_debug_keys) after registration.
Since Fluorine-20130401
val pp_category : Format.formatter -> category -> unit
pretty-prints a category.
Since Chlorine-20180501
val dkey_name : category -> string
returns the category name as a string.
Since 18.0-Argon
val is_registered_category : string -> bool
true iff the string corresponds to a registered category
Since Chlorine-20180501
val get_category : string -> category option
returns the corresponding registered category or None if no such category exists.
Since Fluorine-20130401
Change in Chlorine-20180501: return an option
val get_all_categories : unit -> category list
returns all registered categories.
val add_debug_keys : category -> unit
adds categories corresponding to string (including potential subcategories) to the set of categories for which messages are to be displayed. The string must have been registered beforehand.
Since Fluorine-20130401 use categories instead of plain string
Change in Chlorine-20180501: accepts a string as argument. Takes care of propagating to subcategories.
val del_debug_keys : category -> unit
removes the given categories from the set for which messages are printed. The string must have been registered beforehand.
Since Fluorine-20130401
Change in Chlorine-20180501: accepts a string category as argument, takes care of propagating to subcategories
val get_debug_keys : unit -> category list
Returns currently active keys
Since Fluorine-20130401
Change in Chlorine-20180501: returns a list instead of a set
val is_debug_key_enabled : category -> bool
Returns true if the given category is currently active
Since Fluorine-20130401
val get_debug_keyset : unit -> category list
Deprecated.Fluorine-20130401 use get_debug_keys instead
Returns currently active keys
Since Nitrogen-20111001
val register_warn_category : string -> warn_category
val is_warn_category : string -> bool
val pp_warn_category : Format.formatter -> warn_category -> unit
val pp_all_warn_categories_status : unit -> unit
val wkey_name : warn_category -> string
returns the warning category name as a string.
Since 18.0-Argon
val get_warn_category : string -> warn_category option
val get_all_warn_categories : unit -> warn_category list
val get_all_warn_categories_status : unit -> (warn_category * Log.warn_status) list
val set_warn_status : warn_category -> Log.warn_status -> unit
val get_warn_status : warn_category -> Log.warn_status