Frama-C:
Plug-ins:
Libraries:

Frama-C API - Kernel_log

This modules creates Kernel Logs manually instead of using the one created via the Plugin modules. It is required for Cmdline which cannot depend on Plugin. It also includes all Kernel debug and warning keys. Unless you cannot depend on Frama-C's kernel, always prefere using Kernel instead of Kernel_log.

  • since Frama-C+dev
val kernel_debug_atleast_ref : (int -> bool) Stdlib.ref
  • alert kernel_log Use only in Plugin.
val kernel_verbose_atleast_ref : (int -> bool) Stdlib.ref
  • alert kernel_log Use only in Plugin.
val kernel_channel_name : string

the reserved channel name used by the Frama-C kernel.

val kernel_label_name : string

the reserved label name used by the Frama-C kernel.

include Log.Messages
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
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:(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.

  • since Beryllium-20090601-beta1
val has_tty : unit -> bool

Returns true is this Log's channel is in console mode

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
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
val warning : ?wkey:warn_category -> 'a Log.pretty_printer

Hypothesis and restrictions.

  • since Beryllium-20090601-beta1
val error : 'a Log.pretty_printer

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

  • since Beryllium-20090601-beta1
val abort : ('a, 'b) Log.pretty_aborter

user error stopping the plugin.

  • raises AbortError

    with the channel name.

  • since Beryllium-20090601-beta1
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.

  • raises AbortFatal

    with the channel name.

  • since Beryllium-20090601-beta1
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
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.

  • since Beryllium-20090901
  • before 23.0-Vanadium

    there was no current and source arguments.

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.

  • returns

    the given function itself

  • since Lithium-20081201 in Extlib
  • since Beryllium-20090902
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
val logwith : (Log.event option -> 'b) -> ?wkey:warn_category -> ?emitwith:(Log.event -> unit) -> ?once:bool -> ('a, 'b) Log.pretty_aborter

Recommended 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 : ?help:string -> ?default:bool -> string -> category

register a new debugging/verbose category. Note: to enable a category's messages by default, pass ~default:true or add it (e.g. via add_debug_keys) after registration.

  • since Fluorine-20130401
  • before 30.0-Zinc

    ?help parameter was not present

  • before 32.0-Germanium

    ?default parameter was not present

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

pretty-prints a category.

  • since Chlorine-20180501
val pp_all_categories : unit -> unit

pretty-prints all categories.

  • since 30.0-Zinc
val dkey_name : category -> string

returns the category name as a string.

  • since 18.0-Argon
val get_category_help : category -> string

returns the category help as a string.

  • since Frama-C+dev
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
val get_all_categories : unit -> category list

returns all registered categories.

val add_debug_keys : category -> unit

add_debug_keys s enables the emission of messages for the categories corresponding to s, including potential subcategories (e.g. a and a:b for string a:b). The string must have been registered beforehand.

  • since Fluorine-20130401 use categories instead of plain string
val del_debug_keys : category -> unit

add_debug_keys s disables the emission of messages for the categories corresponding to s, including potential subcategories (e.g. a and a:b for string a:b). The string must have been registered beforehand.

  • since Fluorine-20130401
val get_debug_keys : unit -> category list

Returns currently active keys

  • since Fluorine-20130401
val is_debug_key_enabled : category -> bool

Returns true if the given category is currently active

  • since Fluorine-20130401
val register_warn_category : ?help:string -> ?default:Log.warn_status -> string -> warn_category
  • before 30.0-Zinc

    ?help parameter was not present

  • before 32.0-Germanium

    ?default parameter was not present

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.

  • 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

Message and warning categories

Fclib dkeys

val dkey_task : category
  • before Frama-C+dev

    Was in Task library

val dkey_hptmap : category
val dkey_acsl_extension : category
val dkey_alpha : category
val dkey_alpha_undo : category
val dkey_approximation : category
val dkey_asm_contracts : category
val dkey_ast : category
val dkey_attrs : category

Display debug information related to attributes in Frama-C.

val dkey_builtins : category
val dkey_check : category
val dkey_cil_builder : category
val dkey_cmdline : category
val dkey_constfold : category
val dkey_comments : category
val dkey_compilation_db : category
val dkey_mopsa_db : category
val dkey_mopsa_db_verbose : category
val dkey_dataflow : category
val dkey_dataflow_scc : category
val dkey_dominators : category
val dkey_dyncalls : category
val dkey_emitter : category
val dkey_emitter_clear : category
val dkey_exn_flow : category
val dkey_file_transform : category
val dkey_file_print_one : category
val dkey_file_annot : category
val dkey_file_source : category

Messages related to operations on files during preprocessing/parsing.

val dkey_filter : category
val dkey_inline : category
val dkey_globals : category
val dkey_kf_blocks : category
val dkey_linker : category
val dkey_linker_find : category
val dkey_loops : category
val dkey_pp : category
val dkey_pp_logic : category
val dkey_pretty_source : category
val dkey_print_attrs : category
val dkey_print_bitfields : category
val dkey_print_builtins : category
val dkey_print_logic_coercions : category
val dkey_print_c_types : category
val dkey_print_logic_types : category
val dkey_print_imported_modules : category
val dkey_print_sid : category
val dkey_print_unspecified : category
val dkey_print_vid : category
val dkey_print_field_offsets : category
val dkey_printer_too_early : category
val dkey_prop_status : category
val dkey_prop_status_emit : category
val dkey_prop_status_merge : category
val dkey_prop_status_graph : category
val dkey_prop_status_reg : category
val dkey_project : category
val dkey_rmtmps : category
val dkey_referenced : category
val dkey_typing_global : category
val dkey_typing_init : category
val dkey_typing_chunk : category
val dkey_typing_cast : category
val dkey_typing_pragma : category
val dkey_ulevel : category
val dkey_visitor : category
val dkey_variadic : category
val wkey_annot_error : warn_category

error in annotation. If only a warning, annotation will just be ignored.

val wkey_plugin_not_loaded : warn_category

Warning related to not loaded plugins.

  • since 29.0-Copper
val wkey_extension_unknown : warn_category

Warning related to the use of an unregistered ACSL extension.

  • since 29.0-Copper
val wkey_ghost_already_ghost : warn_category

ghost element is qualified with \ghost while this is already the case by default

val wkey_ghost_bad_use : warn_category

error in ghost code

val wkey_acsl_float_compare : warn_category
val wkey_large_array : warn_category
val wkey_conditional_feature : warn_category

parsing feature that is only supported in specific modes (e.g. C11, gcc, ...).

val wkey_drop_unused : warn_category
val wkey_linker_weak : warn_category
val wkey_implicit_conv_void_ptr : warn_category
val wkey_implicit_int : warn_category
val wkey_incompatible_types_call : warn_category
val wkey_incompatible_pointer_types : warn_category
val wkey_inconsistent_specifier : warn_category
val wkey_int_conversion : warn_category
val wkey_merge_conversion : warn_category
val wkey_alignof_bitfield : warn_category
  • since 32.0-Germanium
val wkey_initializer_overrides : warn_category
val wkey_cert_exp_46 : warn_category
val wkey_cert_msc_37 : warn_category
val wkey_cert_msc_38 : warn_category
val wkey_cert_exp_10 : warn_category
val wkey_check_volatile : warn_category
val wkey_jcdb : warn_category
val wkey_mopsa_db : warn_category
val wkey_mopsa_db_missing_library : warn_category
val wkey_mopsa_db_non_c : warn_category
val wkey_implicit_function_declaration : warn_category
val wkey_no_proto : warn_category
val wkey_missing_spec : warn_category
val wkey_multi_from : warn_category
val wkey_decimal_float : warn_category
val wkey_acsl_extension : warn_category
val wkey_cmdline : warn_category

Command-line related warning, e.g. for invalid options given by the user

val wkey_audit : warn_category

Warning related to options '-audit-*'.

val wkey_parser_unsupported : warn_category

Warning related to unsupported parsing-related features.

val wkey_parser_unsupported_attributes : warn_category

Warning related to unsupported attributes during parsing.

val wkey_parser_unsupported_pragma : warn_category

Warning related to unsupported _Pragma's during parsing.

val wkey_asm : warn_category

Warnings related to assembly code.

val wkey_unnamed_typedef : warn_category

Warning related to "unnamed typedef that does not introduce a struct or enumeration type".

val wkey_file_not_found : warn_category

Warnings related to missing files during preprocessing/parsing.

val wkey_c11 : warn_category

Warnings related to usage of C11-specific constructions.

val wkey_line_directive : warn_category

Warnings related to unknown line directives.

val wkey_attrs : warn_category

Warning related to the handling of attributes in Frama-C.

val wkey_unknown_attribute : warn_category

Warning emitted when an unknown attribute is encountered during parsing.

val wkey_long_double : warn_category

Warning emitted by plugins that do not support the long double format.

val wkey_format : warn_category
val wkey_libc : warn_category
val wkey_libc_framac : warn_category
val wkey_prototype : warn_category
val wkey_typing : warn_category
val wkey_variadic_format_nonliteral : warn_category
val wkey_transient : warn_category
val wkey_inline : warn_category
val wkey_project : warn_category