Frama-C API - `Kernel`

Provided services for kernel developers.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Log Machinery

include Plugin.S

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

Hypothesis and restrictions.

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val error : 'a Log.pretty_printer

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

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val abort : ('a, 'b) Log.pretty_aborter

user error stopping the plugin.

raises AbortError
with the channel name.

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val failure : 'a Log.pretty_printer

internal error of the plug-in.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val fatal : ('a, 'b) Log.pretty_aborter

internal error of the plug-in.

raises AbortFatal
with the channel name.

since Beryllium-20090601-beta1

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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.

since 18.0-Argon

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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.

since Fluorine-20130401

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

pretty-prints a category.

since Chlorine-20180501

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

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.

since Fluorine-20130401 use categories instead of plain string

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.

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 : string -> warn_category

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

since Beryllium-20090901

module Verbose : Parameter_sig.Int

module Debug : Parameter_sig.Int

module Share : Parameter_sig.Specific_dir

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

module Session : Parameter_sig.Specific_dir

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

module Config : Parameter_sig.Specific_dir

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

val help : Cmdline.Group.t

The group containing option -*-help.

since Boron-20100401

val messages : Cmdline.Group.t

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

since Boron-20100401

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.

Message and warning categories

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

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

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

module Kernel_function_set (_ : Input_with_arg) : Parameter_sig.Kernel_function_set

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"

module PrintShare : Parameter_sig.Bool

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

Directory in which session files are searched.

module Config_dir : Parameter_sig.Filepath

Directory in which config files are searched.

module Set_project_as_default : Parameter_sig.Bool

Undocumented.

Customizing Normalization and parsing

module UnrollingLevel : Parameter_sig.Int

Behavior of option "-ulevel"

module UnrollingForce : 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 ContinueOnAnnotError : Parameter_sig.Bool

Behavior of option "-continue-annot-error"

module SimplifyCfg : Parameter_sig.Bool

Behavior of option "-simplify-cfg"

module KeepSwitch : Parameter_sig.Bool

Behavior of option "-keep-switch"

module Keep_unused_specified_functions : Parameter_sig.Bool

Behavior of option "-keep-unused-specified-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"

module InitializedPaddingLocals : Parameter_sig.Bool

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"

module AsmContractsAutoValidate : Parameter_sig.Bool

Behavior of option "-asm-contracts-auto-validate."

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 WarnDecimalFloat : Parameter_sig.String

Behavior of option "-warn-decimal-float"

module ImplicitFunctionDeclaration : Parameter_sig.String

Behavior of option "-implicit-function-declaration"

module C11 : Parameter_sig.Bool

Behavior of option "-c11"

module JsonCompilationDatabase : Parameter_sig.Filepath

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"

Frama-C API - Kernel