Module Kernel

module Kernel: sig .. end

Provided services for kernel developers.


Log Machinery

include Plugin.S

Message and warning categories

val dkey_alpha : category
val dkey_alpha_undo : category
val dkey_asm_contracts : category
val dkey_ast : category
val dkey_check : 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_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_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_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_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_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_drop_unused : 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_cert_exp_46 : warn_category
val wkey_cert_msc_38 : 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_decimal_float : warn_category

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: 
functor (X : 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 PrintConfig: Parameter_sig.Bool 

Behavior of option "-print-config"

module PrintVersion: Parameter_sig.Bool 

Behavior of option "-print-version"

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"

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 Unicode: sig .. end

Behavior of option "-unicode".

module UseUnicode: Parameter_sig.Bool 

Behavior of option "-unicode"

module Time: Parameter_sig.String 

Behavior of option "-time"

Input / Output Source Code

module PrintCode: Parameter_sig.Bool 

Behavior of option "-print"

module PrintMachdep: Parameter_sig.Bool 

Behavior of option "-print-machdep"

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 SymbolicPath: Parameter_sig.String_set 

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"

Save/Load

module SaveState: Parameter_sig.String 

Behavior of option "-save"

module LoadState: Parameter_sig.String 

Behavior of option "-load"

module LoadModule: Parameter_sig.String_list 

Behavior of option "-load-module"

module AutoLoadPlugins: Parameter_sig.Bool 

Behavior of option "-autoload-plugins"

module Journal: sig .. end

Kernel for journalization.

module Session_dir: Parameter_sig.String 

Directory in which session files are searched.

module Config_dir: Parameter_sig.String 

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

module LogicalOperators: Parameter_sig.Bool 

Behavior of invisible option -keep-logical operator: Tries to avoid converting && and || into conditional statements.

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 CppGnuLike: Parameter_sig.Bool 

Behavior of option "-cpp-frama-c-compliant"

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-function".

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.String_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: State_builder.Ref  with type data = string

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

Analysis Behavior of options

module MainFunction: sig .. end

Behavior of option "-main".

module LibEntry: sig .. end

Behavior of option "-lib-entry".

module ConstReadonly: Parameter_sig.Bool 

Global variables with "const" qualifier are constant.

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 SignedDowncast: Parameter_sig.Bool 

Behavior of option "-warn-signed-downcast"

module UnsignedDowncast: Parameter_sig.Bool 

Behavior of option "-warn-unsigned-downcast"

module SpecialFloat: Parameter_sig.String 

Behavior of option "-warn-special-float"

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"