Functor Log.Register

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.

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.

type warn_category 

Same as above, but for warnings

val verbose_atleast : int -> bool
val debug_atleast : int -> bool
val printf : ?level:int ->
?dkey:category ->
?current:bool ->
?source:Lexing.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.

val feedback : ?ontty:Log.ontty ->
?level:int -> ?dkey:category -> 'a Log.pretty_printer

Progress and feedback. Level is tested against the verbosity level.

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.

val warning : ?wkey:warn_category -> 'a Log.pretty_printer

Hypothesis and restrictions.

val error : 'a Log.pretty_printer

user error: syntax/typing error, bad expected input, etc.

val abort : ('a, 'b) Log.pretty_aborter

user error stopping the plugin.

val failure : 'a Log.pretty_printer

internal error of the plug-in.

val fatal : ('a, 'b) Log.pretty_aborter

internal error of the plug-in.

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

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.

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.

val with_result : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
val with_warning : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
val with_error : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
val with_failure : (Log.event -> 'b) -> ('a, 'b) Log.pretty_aborter
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):

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.

val pp_category : Format.formatter -> category -> unit

pretty-prints a category.

val is_registered_category : string -> bool

true iff the string corresponds to a registered category

val get_category : string -> category option

returns the corresponding registered category or None if no such category exists.

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.

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.

val get_debug_keys : unit -> category list

Returns currently active keys

val is_debug_key_enabled : category -> bool

Returns true if the given category is currently active

val get_debug_keyset : unit -> category list
Deprecated.Fluorine-20130401 use get_debug_keys instead

Returns currently active keys

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