Module type Log.Messages

module type Messages = sig .. 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:Filepath.position ->
?append:(Stdlib.Format.formatter -> unit) ->
?header:(Stdlib.Format.formatter -> unit) ->
('a, Stdlib.Format.formatter, unit) Stdlib.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 : ?current:bool ->
?source:Filepath.position ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.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 option -> 'b) -> ('a, 'b) Log.pretty_aborter

with_result f fmt calls f in the same condition as logwith.

val with_warning : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter

with_warning f fmt calls f in the same condition as logwith.

val with_error : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter

with_error f fmt calls f in the same condition as logwith.

val with_failure : (Log.event option -> 'b) -> ('a, 'b) Log.pretty_aborter

with_failure f fmt calls f in the same condition as logwith.

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

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 : Stdlib.Format.formatter -> category -> unit

pretty-prints a category.

val dkey_name : category -> string

returns the category name as a string.

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 : Stdlib.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.

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