Frama-C API - Wp_parameters
WP Plugin Interface
include Frama_c_kernel.Plugin.S
include Frama_c_kernel.Log.Messages
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.
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 result : ?level:int -> ?dkey:category -> 'a Frama_c_kernel.Log.pretty_printer
Results of analysis. Default level is 1.
val feedback : ?ontty:Frama_c_kernel.Log.ontty -> ?level:int -> ?dkey:category -> 'a Frama_c_kernel.Log.pretty_printer
Progress and feedback. Level is tested against the verbosity level.
val debug : ?level:int -> ?dkey:category -> 'a Frama_c_kernel.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 Frama_c_kernel.Log.pretty_printer
Hypothesis and restrictions.
val error : 'a Frama_c_kernel.Log.pretty_printer
user error: syntax/typing error, bad expected input, etc.
val abort : ('a, 'b) Frama_c_kernel.Log.pretty_aborter
user error stopping the plugin.
val failure : 'a Frama_c_kernel.Log.pretty_printer
internal error of the plug-in.
val fatal : ('a, 'b) Frama_c_kernel.Log.pretty_aborter
internal error of the plug-in.
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...") ;
.
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.
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 : (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
.
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
.
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
.
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
.
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 leastn
.log ~debug:n
: emit the message only when debugging level is at leastn
.log ~verbose:n ~debug:m
: any debugging or verbosity level is sufficient.
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
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 : Frama_c_kernel.Log.kind -> (Frama_c_kernel.Log.event -> unit) -> unit
Local registry for listeners.
Category management
val register_category : ?help:string -> string -> category
register a new debugging/verbose category. Note: to enable a category's messages by default, add it (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 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
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.
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.
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 register_warn_category : ?help:string -> string -> warn_category
val pp_warn_category : Stdlib.Format.formatter -> warn_category -> 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 * Frama_c_kernel.Log.warn_status) list
val set_warn_status : warn_category -> Frama_c_kernel.Log.warn_status -> unit
val get_warn_status : warn_category -> Frama_c_kernel.Log.warn_status
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
module Verbose : Frama_c_kernel.Parameter_sig.Int
module Debug : Frama_c_kernel.Parameter_sig.Int
Handle the specific `share' directory of the plug-in.
Handle the specific `session' directory of the plug-in.
module Cache_dir () : Frama_c_kernel.Parameter_sig.User_dir_opt
Handle the specific `cache' directory of the plug-in.
module Config_dir () : Frama_c_kernel.Parameter_sig.User_dir_opt
Handle the specific `config' directory of the plug-in.
module State_dir () : Frama_c_kernel.Parameter_sig.User_dir_opt
Handle the specific `state' directory of the plug-in.
val help : Frama_c_kernel.Cmdline.Group.t
The group containing option -*-help.
val messages : Frama_c_kernel.Cmdline.Group.t
The group containing options -*-debug and -*-verbose.
val hypothesis : 'a Frama_c_kernel.Log.pretty_printer
Function Selection
type functions =
| Fct_none
| Fct_all
| Fct_skip of Frama_c_kernel.Cil_datatype.Kf.Set.t
| Fct_list of Frama_c_kernel.Cil_datatype.Kf.Set.t
val get_fct : unit -> functions
val iter_fct : (Frama_c_kernel.Kernel_function.t -> unit) -> functions -> unit
val iter_kf : (Frama_c_kernel.Kernel_function.t -> unit) -> unit
Goal Selection
module WP : Frama_c_kernel.Parameter_sig.Bool
module Dump : Frama_c_kernel.Parameter_sig.Bool
Model Selection
val has_dkey : category -> bool
Computation Strategies
module Init : Frama_c_kernel.Parameter_sig.Bool
module RTE : Frama_c_kernel.Parameter_sig.Bool
module Simpl : Frama_c_kernel.Parameter_sig.Bool
module Let : Frama_c_kernel.Parameter_sig.Bool
module Core : Frama_c_kernel.Parameter_sig.Bool
module Prune : Frama_c_kernel.Parameter_sig.Bool
module Clean : Frama_c_kernel.Parameter_sig.Bool
module Filter : Frama_c_kernel.Parameter_sig.Bool
module Prenex : Frama_c_kernel.Parameter_sig.Bool
module Ground : Frama_c_kernel.Parameter_sig.Bool
module Reduce : Frama_c_kernel.Parameter_sig.Bool
module SplitMax : Frama_c_kernel.Parameter_sig.Int
module SplitCNF : Frama_c_kernel.Parameter_sig.Int
module DynCall : Frama_c_kernel.Parameter_sig.Bool
Prover Interface
module Detect : Frama_c_kernel.Parameter_sig.Bool
module Cache : Frama_c_kernel.Parameter_sig.String
module Timeout : Frama_c_kernel.Parameter_sig.Int
module Memlimit : Frama_c_kernel.Parameter_sig.Int
module FctTimeout : Frama_c_kernel.Parameter_sig.Map with type key = Frama_c_kernel.Cil_types.kernel_function and type value = int
module Steps : Frama_c_kernel.Parameter_sig.Int
module Procs : Frama_c_kernel.Parameter_sig.Int
Proof Obligations
module Print : Frama_c_kernel.Parameter_sig.Bool
module Status : Frama_c_kernel.Parameter_sig.Bool
module Probes : Frama_c_kernel.Parameter_sig.Bool
Getters
val get_session : force:bool -> unit -> Frama_c_kernel.Datatype.Filepath.t
val get_session_dir : force:bool -> string -> Frama_c_kernel.Datatype.Filepath.t
val get_output : unit -> Frama_c_kernel.Datatype.Filepath.t
val get_output_dir : string -> Frama_c_kernel.Datatype.Filepath.t
val make_output_dir : Frama_c_kernel.Datatype.Filepath.t -> unit
Debugging Categories
val print_generated : ?header:string -> Frama_c_kernel.Filepath.Normalized.t -> unit
print the given file if the debugging category "print-generated" is set
val cat_print_generated : category