Frama-C API - Kernel
Provided services for kernel developers.
Log Machinery
include Plugin.S
include 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: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.
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
):
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 : (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.
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 * Log.warn_status) list
val set_warn_status : warn_category -> Log.warn_status -> unit
val get_warn_status : warn_category -> Log.warn_status
include Plugin.S_no_log
val add_group : ?memo:bool -> string -> 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 : Parameter_sig.Int
module Debug : Parameter_sig.Int
Handle the specific `share' directory of the plug-in.
module Session : Parameter_sig.User_dir_opt
Handle the specific `session' directory of the plug-in.
val help : Cmdline.Group.t
The group containing option -*-help.
val messages : Cmdline.Group.t
The group containing options -*-debug and -*-verbose.
Message and warning categories
val dkey_acsl_extension : category
val dkey_alpha : category
val dkey_alpha_undo : category
val dkey_asm_contracts : category
val dkey_ast : category
val dkey_builtins : category
val dkey_check : category
val dkey_constfold : category
val dkey_comments : category
val dkey_compilation_db : 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_globals : category
val dkey_kf_blocks : category
val dkey_linker : category
val dkey_linker_find : category
val dkey_loops : category
val dkey_parser : category
val dkey_pp : category
val dkey_pp_logic : 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_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_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_rmtmps : category
val dkey_referenced : category
val dkey_task : 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 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.
val wkey_extension_unknown : warn_category
Warning related to the use of an unregistered ACSL extension.
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_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_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_unknown_attribute : warn_category
Warning emitted when an unknown attribute is encountered during parsing.
Functors for late option registration
Kernel_function-related options cannot be registered in this module: They depend on Globals
, which is linked later. We provide here functors to declare them after Globals
module type Input_with_arg = sig ... end
Option groups
val inout_source : Cmdline.Group.t
val saveload : Cmdline.Group.t
val parsing : Cmdline.Group.t
val normalisation : Cmdline.Group.t
val analysis_options : Cmdline.Group.t
val seq : Cmdline.Group.t
val project : Cmdline.Group.t
val checks : Cmdline.Group.t
Installation Information
module Version : Parameter_sig.Bool
Behavior of option "-version"
module PrintVersion : Parameter_sig.Bool
Behavior of option "-print-version"
module PrintConfig : Parameter_sig.Bool
Behavior of option "-print-config"
Behavior of option "-print-share-path"
module PrintLib : Parameter_sig.Bool
Behavior of option "-print-lib-path"
module PrintPluginPath : Parameter_sig.Bool
Behavior of option "-print-plugin-path"
module AutocompleteHelp : Parameter_sig.String_set
Behavior of option "-autocomplete"
module PrintConfigJson : Parameter_sig.Bool
Behavior of option "-print-config-json"
Output Messages
module GeneralVerbose : Parameter_sig.Int
Behavior of option "-verbose"
module GeneralDebug : Parameter_sig.Int
Behavior of option "-debug"
module Quiet : Parameter_sig.Bool
Behavior of option "-quiet"
module Permissive : Parameter_sig.Bool
Behavior of option "-permissive"
module Unicode : sig ... end
module Time : Parameter_sig.String
Behavior of option "-time"
Input / Output Source Code
module PrintCode : Parameter_sig.Bool
Behavior of option "-print"
module PrintAsIs : Parameter_sig.Bool
Behavior of option "-print-as-is"
module PrintMachdep : Parameter_sig.Bool
Behavior of option "-print-machdep"
module PrintMachdepHeader : Parameter_sig.Bool
Behavior of option "-print-machdep-header"
module PrintLibc : Parameter_sig.Bool
Behavior of option "-print-libc"
module PrintComments : Parameter_sig.Bool
Behavior of option "-keep-comments"
module PrintReturn : Parameter_sig.Bool
Behavior of option "-print-return"
module CodeOutput : sig ... end
Behavior of option "-ocode".
module AstDiff : Parameter_sig.Bool
Behavior of option "-ast-diff"
module SymbolicPath : Parameter_sig.Filepath_map with type value = string
Behavior of option "-add-symbolic-path"
module FloatNormal : Parameter_sig.Bool
Behavior of option "-float-normal"
module FloatRelative : Parameter_sig.Bool
Behavior of option "-float-relative"
module FloatHex : Parameter_sig.Bool
Behavior of option "-float-hex"
module BigIntsHex : Parameter_sig.Int
Behavior of option "-hexadecimal-big-integers"
module EagerLoadSources : Parameter_sig.Bool
Behavior of option "-eager-load-sources"
Save/Load
module SaveState : Parameter_sig.Filepath
Behavior of option "-save"
module LoadState : Parameter_sig.Filepath
Behavior of option "-load"
module LoadModule : Parameter_sig.String_list
Behavior of option "-load-module"
module LoadLibrary : Parameter_sig.String_list
Behavior of option "-load-library"
module AutoLoadPlugins : Parameter_sig.Bool
Behavior of option "-autoload-plugins"
module Session_dir : Parameter_sig.User_dir
Directory in which session files are searched.
module Cache_dir : Parameter_sig.User_dir
Directory in which cache files are searched.
module Config_dir : Parameter_sig.User_dir
Directory in which config files are searched.
module State_dir : Parameter_sig.User_dir
Directory in which state files are searched.
module Set_project_as_default : Parameter_sig.Bool
Undocumented.
Customizing Normalization and parsing
module UnfoldingLevel : Parameter_sig.Int
Behavior of option "-ulevel"
module UnfoldingForce : Parameter_sig.Bool
Behavior of option "-ulevel-force"
module Machdep : Parameter_sig.String
Behavior of option "-machdep". If function set
is called, then File.prepare_from_c_files
must be called for well preparing the AST.
module LogicalOperators : Parameter_sig.Bool
Behavior of invisible option -keep-logical-operators: Tries to avoid converting && and || into conditional statements. Note that this option is incompatible with many (most) plug-ins of the platform and thus should only be enabled with great care and for very specific analyses need.
module Enums : Parameter_sig.String
Behavior of option "-enums"
module CppCommand : Parameter_sig.String
Behavior of option "-cpp-command"
module CppExtraArgs : Parameter_sig.String_list
Behavior of option "-cpp-extra-args"
module CppExtraArgsPerFile : Parameter_sig.Filepath_map with type value = string
Behavior of option "-cpp-extra-args-per-file"
module CppGnuLike : Parameter_sig.Bool
Behavior of option "-cpp-frama-c-compliant"
module PrintCppCommands : Parameter_sig.Bool
Behavior of option "-print-cpp-commands"
module AuditPrepare : Parameter_sig.Filepath
Behavior of option "-audit-prepare"
module AuditCheck : Parameter_sig.Filepath
Behavior of option "-audit-check"
module FramaCStdLib : Parameter_sig.Bool
Behavior of option "-frama-c-stdlib"
module ReadAnnot : Parameter_sig.Bool
Behavior of option "-read-annot"
module PreprocessAnnot : Parameter_sig.Bool
Behavior of option "-pp-annot"
module SimplifyCfg : Parameter_sig.Bool
Behavior of option "-simplify-cfg"
module KeepSwitch : Parameter_sig.Bool
Behavior of option "-keep-switch"
module KeepUnusedFunctions : Parameter_sig.String
Behavior of option "-keep-unused-functions".
module Keep_unused_types : Parameter_sig.Bool
Behavior of option "-keep-unused-types".
module SimplifyTrivialLoops : Parameter_sig.Bool
Behavior of option "-simplify-trivial-loops".
module Constfold : Parameter_sig.Bool
Behavior of option "-constfold"
Behavior of option "-initialized-padding-locals"
module AggressiveMerging : Parameter_sig.Bool
Behavior of option "-aggressive-merging"
module AsmContractsGenerate : Parameter_sig.Bool
Behavior of option "-asm-contracts"
Behavior of option "-asm-contracts-ensure-init"
Behavior of option "-asm-contracts-auto-validate"
module InlineStmtContracts : Parameter_sig.Bool
Behavior of option "-inline-stmt-contracts"
module RemoveExn : Parameter_sig.Bool
Behavior of option "-remove-exn"
module Files : Parameter_sig.Filepath_list
Analyzed files
module Orig_name : Parameter_sig.Bool
Behavior of option "-orig-name"
val normalization_parameters : unit -> Typed_parameter.t list
All the normalization options that influence the AST (in particular, changing one will reset the AST entirely.contents
module C11 : Parameter_sig.Bool
Behavior of option "-c11"
Behavior of option "-json-compilation-database"
Customizing cabs2cil options
module AllowDuplication : Parameter_sig.Bool
Behavior of option "-allow-duplication".
module DoCollapseCallCast : Parameter_sig.Bool
Behavior of option "-collapse-call-cast".
module GeneratedSpecMode : Parameter_sig.String
Behavior of option "-generated-spec-mode".
module GeneratedSpecCustom : Parameter_sig.Map with type key = string and type value = string
Behavior of option "-generated-spec-custom".
Analysis Behavior of options
module MainFunction : sig ... end
Behavior of option "-main".
module LibEntry : sig ... end
Behavior of option "-lib-entry".
module UnspecifiedAccess : Parameter_sig.Bool
Behavior of option "-unspecified-access"
module SafeArrays : Parameter_sig.Bool
Behavior of option "-safe-arrays".
module SignedOverflow : Parameter_sig.Bool
Behavior of option "-warn-signed-overflow"
module UnsignedOverflow : Parameter_sig.Bool
Behavior of option "-warn-unsigned-overflow"
module LeftShiftNegative : Parameter_sig.Bool
Behavior of option "-warn-left-shift-negative"
module RightShiftNegative : Parameter_sig.Bool
Behavior of option "-warn-right-shift-negative"
module SignedDowncast : Parameter_sig.Bool
Behavior of option "-warn-signed-downcast"
module UnsignedDowncast : Parameter_sig.Bool
Behavior of option "-warn-unsigned-downcast"
module PointerDowncast : Parameter_sig.Bool
Behavior of option "-warn-pointer-downcast"
module SpecialFloat : Parameter_sig.String
Behavior of option "-warn-special-float"
module InvalidBool : Parameter_sig.Bool
Behavior of option "-warn-invalid-bool"
module InvalidPointer : Parameter_sig.Bool
Behavior of option "-warn-invalid-pointer"
module AbsoluteValidRange : Parameter_sig.String
Behavior of option "-absolute-valid-range"
Checks
module Check : Parameter_sig.Bool
Behavior of option "-check"
module Copy : Parameter_sig.Bool
Behavior of option "-copy"
module TypeCheck : Parameter_sig.Bool
Behavior of option "-typecheck"