Frama-C:
Plug-ins:
Libraries:

Frama-C API - Self

include Frama_c_kernel.Plugin.General_services
include Frama_c_kernel.Plugin.S
include Frama_c_kernel.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:Frama_c_kernel.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 has_tty : unit -> bool

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

val verify : bool -> ('a, bool) Frama_c_kernel.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:Frama_c_kernel.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 : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

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

  • since Beryllium-20090601-beta1
val with_warning : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

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

  • since Beryllium-20090601-beta1
val with_error : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

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

  • since Beryllium-20090601-beta1
val with_failure : (Frama_c_kernel.Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel.Log.pretty_aborter

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

  • since Beryllium-20090601-beta1
val log : ?kind:Frama_c_kernel.Log.kind -> ?verbose:int -> ?debug:int -> 'a Frama_c_kernel.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 : (Frama_c_kernel.Log.event option -> 'b) -> ?wkey:warn_category -> ?emitwith:(Frama_c_kernel.Log.event -> unit) -> ?once:bool -> ('a, 'b) Frama_c_kernel.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 : Frama_c_kernel.Log.kind -> (Frama_c_kernel.Log.event -> unit) -> unit

Local registry for listeners.

val register_tag_handlers : ((string -> string) * (string -> string)) -> unit

Category management

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 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 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 * Frama_c_kernel.Log.warn_status) list
val set_warn_status : warn_category -> Frama_c_kernel.Log.warn_status -> unit
include Frama_c_kernel.Plugin.S_no_log
val add_group : ?memo:bool -> string -> Frama_c_kernel.Cmdline.Group.t

Create a new group inside the plug-in. The given string must be different of all the other group names of this plug-in if memo is false. If memo is true the function will either create a fresh group or return an existing group of the same name in the same plugin. memo defaults to false

  • since Beryllium-20090901

Handle the specific `lib' directory of the plug-in.

Handle the specific `share' directory of the plug-in.

Handle the specific `session' directory of the plug-in.

Handle the specific `cache' directory of the plug-in.

Handle the specific `config' directory of the plug-in.

Handle the specific `state' directory of the plug-in.

The group containing option -*-help.

  • since Boron-20100401

The group containing options -*-debug and -*-verbose.

  • since Boron-20100401

Group containing debug options.

  • since 32.0-Germanium
val add_plugin_output_aliases : ?visible:bool -> ?deprecated:bool -> string list -> unit

Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log, -plugin-msg-key, and -plugin-warn-key. add_plugin_output_aliases [alias] adds the aliases -alias-help, -alias-verbose, etc.

  • since 18.0-Argon
  • before 22.0-Titanium

    no visible and deprecated arguments.

include Frama_c_kernel.Parameter_sig.Builder
module Bool (_ : sig ... end) : Frama_c_kernel.Parameter_sig.Bool
module Int (_ : sig ... end) : Frama_c_kernel.Parameter_sig.Int
module Float (_ : sig ... end) : Frama_c_kernel.Parameter_sig.Float

Parameter with an optional decimal point converted to an Ocaml float

Builds a Site_dir from an existing one. The first parameter is the parent directory. The second gives the name of the directory to create.

Builds a User_dir from an existing one. The first parameter is the parent directory. The second gives the name of the directory to create.

Builds a User_dir_opt from an existing User_dir. The first parameter is the parent directory. The second gives the name of the directory to create (also used to create the option name), a possible environment variable name and the help message for the option.

Allow using custom types as parameters.

module Enum (X : sig ... end) : Frama_c_kernel.Parameter_sig.S with type t = X.t

A fixed set of possible values, represented by a type t, intended to be a variant with only a finite number of possible constructions. Note that t must be comparable with structural equality

exception Cannot_build of string
module Make_list (E : sig ... end) (_ : sig ... end) : Frama_c_kernel.Parameter_sig.List with type elt = E.t and type t = E.t list

Parameter is a map where multibindings are **not** allowed.

As for Kernel_function_set, by default keys can only be defined functions. Use Parameter_customize.argument_may_be_fundecl to also include pure prototypes.

Parameter is a map where multibindings are allowed.

As for Kernel_function_set, by default keys can only be defined functions. Use Parameter_customize.argument_may_be_fundecl to also include pure prototypes.

val parameters : unit -> Frama_c_kernel.Typed_parameter.t list
val is_computed : unit -> bool

Return true iff the value analysis has been done.

val clear_results : unit -> unit

Clears the results of the Eva analysis.

type computation_state =
  1. | NotComputed
  2. | Computing
  3. | Computed
  4. | Aborted

Computation state of the analysis.

The current computation state of the analysis, updated by force_compute and states updates.

exception Abort

Exception used to cleanly abort the analysis (without killing Frama-C).

val dkey_initial_state : category

Debug categories responsible for printing initial and final states of Value. Enabled by default, but can be disabled via the command-line: -value-msg-key="-initial_state,-final_state"

val dkey_final_states : category
val dkey_summary : category

Debug categories.

val register_category : help:string -> ?default:bool -> string -> category

Same as Log's register_category, but help is mandatory.

val dkey_pointer_comparison : category
val dkey_cvalue_domain : category
val dkey_iterator : category
val dkey_widening : category
val dkey_partition : category
val dkey_split_return : category
val dkey_precision_settings : category
val dkey_callstacks : category
val dkey_callstack_hash : category
val dkey_include_string_literal : category

Warning categories.

val register_warn_category : help:string -> ?default:Frama_c_kernel.Log.warn_status -> string -> warn_category

Same as Log's register_warn_category, but help is mandatory.

val wkey_alarm : warn_category
val wkey_locals_escaping : warn_category
val wkey_garbled_mix_write : warn_category
val wkey_garbled_mix_assigns : warn_category
val wkey_garbled_mix_summary : warn_category
val wkey_builtins_missing_spec : warn_category
val wkey_builtins_override : warn_category
val wkey_libc_unsupported_spec : warn_category
val wkey_loop_unroll_auto : warn_category
val wkey_loop_unroll_partial : warn_category
val wkey_missing_loop_unroll : warn_category
val wkey_missing_loop_unroll_for : warn_category
val wkey_signed_overflow : warn_category
val wkey_invalid_assigns : warn_category
val wkey_missing_assigns : warn_category
val wkey_missing_assigns_result : warn_category
val wkey_experimental : warn_category
val wkey_unknown_size : warn_category
val wkey_ensures_false : warn_category
val wkey_watchpoint : warn_category
val wkey_recursion : warn_category
val wkey_acsl : warn_category
val wkey_acsl_unsupported : warn_category

Logging.

This modules adapt the interface of Log.Messages to be usable with Position.t.

If position is given, then message will be located at this position. Otherwise if current or source are given, then the current position tracked by the kernel or the given location will respectively be used. stacktrace optional parameter controls whether the call stack must be printed at the end of the message and always default to false.

See Log.Messages for documentation

type 'a pretty_printer = ?emitwith:(Frama_c_kernel.Log.event -> unit) -> ?once:bool -> ?pos:Position.t -> ?current:bool -> ?source:Frama_c_kernel.Fclib.Filepath.position -> ?stacktrace:bool -> ?append:(Stdlib.Format.formatter -> unit) -> ?echo:bool -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a
type ('a, 'b) pretty_aborter = ?pos:Position.t -> ?current:bool -> ?source:Frama_c_kernel.Fclib.Filepath.position -> ?stacktrace:bool -> ?append:(Stdlib.Format.formatter -> unit) -> ?echo:bool -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
val result : ?level:int -> ?dkey:category -> 'a pretty_printer

Results of analysis.

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

Progress and feedback.

val debug : ?level:int -> ?dkey:category -> 'a pretty_printer

Debugging information.

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

Warnings.

val alarm : 'a pretty_printer

Alarm emitted by the analysis.

val error : 'a pretty_printer

User error.

val abort : ('a, 'b) pretty_aborter

User error stopping the plugin.

val failure : 'a pretty_printer

Internal error of the plug-in.

val fatal : ('a, 'b) pretty_aborter

Internal error stopping the plug-in.