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.
This functor should not be directly applied by plug-in developer.
They should apply
Plugin.Register
instead.
Since Beryllium-20090601-beta1
Parameters: |
P |
: |
sig
val channel : string
val label : string
val verbose_atleast : int -> bool
val debug_atleast : int -> bool
end
|
|
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
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
):
log ~verbose:n
: emit the message only when verbosity level is
at least n
.
log ~debug:n
: emit the message only when debugging level is
at least n
.
log ~verbose:n ~debug:m
: any debugging or verbosity level is
sufficient.
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