module Kernel:sig
..end
Provided services for kernel developers.
include Plugin.S
val dkey_alpha : category
val dkey_alpha_undo : category
val dkey_asm_contracts : category
val dkey_ast : 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_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_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_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_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_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_cert_exp_46 : 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
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:
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
module PrintConfig:Parameter_sig.Bool
Behavior of option "-print-config"
module PrintVersion:Parameter_sig.Bool
Behavior of option "-print-version"
: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"
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
Behavior of option "-unicode".
module UseUnicode:Parameter_sig.Bool
Behavior of option "-unicode"
module Time:Parameter_sig.String
Behavior of option "-time"
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"
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 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.
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-operators: 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 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 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
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
module ImplicitFunctionDeclaration:Parameter_sig.String
module C11:Parameter_sig.Bool
Behavior of option "-c11"
module JsonCompilationDatabase:Parameter_sig.Filepath
Behavior of option "-json-compilation-database"
module AllowDuplication:Parameter_sig.Bool
Behavior of option "-allow-duplication".
module DoCollapseCallCast:Parameter_sig.Bool
Behavior of option "-collapse-call-cast".
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"
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"