Module Value_parameters

module Value_parameters: sig .. end

include Plugin.General_services
module ForceValues: Parameter_sig.With_output 
module EnumerateCond: Parameter_sig.Bool 
module OracleDepth: Parameter_sig.Int 
module ReductionDepth: Parameter_sig.Int 
module Domains: Parameter_sig.String_set 
module DomainsFunction: Parameter_sig.Multiple_map 
  with type key = string
   and type value = Domain_mode.function_mode
module EqualityCall: Parameter_sig.String 
module EqualityCallFunction: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = string
module OctagonCall: Parameter_sig.Bool 
module TracesUnrollLoop: Parameter_sig.Bool 
module TracesUnifyLoop: Parameter_sig.Bool 
module TracesDot: Parameter_sig.Filepath 
module TracesProject: Parameter_sig.Bool 
module AutomaticContextMaxDepth: Parameter_sig.Int 
module AutomaticContextMaxWidth: Parameter_sig.Int 
module AllRoundingModesConstants: Parameter_sig.Bool 
module NoResultsDomains: Parameter_sig.String_set 
module NoResultsFunctions: Parameter_sig.Fundec_set 
module ResultsAll: Parameter_sig.Bool 
module JoinResults: Parameter_sig.Bool 
module WarnSignedConvertedDowncast: Parameter_sig.Bool 
module WarnPointerSubstraction: Parameter_sig.Bool 
module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set 
module DescendingIteration: Parameter_sig.String 
module HierarchicalConvergence: Parameter_sig.Bool 
module WideningDelay: Parameter_sig.Int 
module WideningPeriod: Parameter_sig.Int 
module RecursiveUnroll: Parameter_sig.Int 
module SemanticUnrollingLevel: Parameter_sig.Int 
module SlevelFunction: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = int
module SlevelMergeAfterLoop: Parameter_sig.Kernel_function_set 
module MinLoopUnroll: Parameter_sig.Int 
module AutoLoopUnroll: Parameter_sig.Int 
module DefaultLoopUnroll: Parameter_sig.Int 
module HistoryPartitioning: Parameter_sig.Int 
module ValuePartitioning: Parameter_sig.String_set 
module SplitLimit: Parameter_sig.Int 
module InterproceduralSplits: Parameter_sig.Bool 
module InterproceduralHistory: Parameter_sig.Bool 
module ArrayPrecisionLevel: Parameter_sig.Int 
module AllocatedContextValid: Parameter_sig.Bool 
module InitializationPaddingGlobals: Parameter_sig.String 
module Numerors_Real_Size: Parameter_sig.Int 
module Numerors_Mode: Parameter_sig.String 
module UndefinedPointerComparisonPropagateAll: Parameter_sig.Bool 
module WarnPointerComparison: Parameter_sig.String 
module ReduceOnLogicAlarms: Parameter_sig.Bool 
module InitializedLocals: Parameter_sig.Bool 
module UsePrototype: Parameter_sig.Kernel_function_set 
module SkipLibcSpecs: Parameter_sig.Bool 
module RmAssert: Parameter_sig.Bool 
module LinearLevel: Parameter_sig.Int 
module LinearLevelFunction: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = int
module BuiltinsOverrides: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = string
module BuiltinsAuto: Parameter_sig.Bool 
module BuiltinsList: Parameter_sig.Bool 
module SplitReturnFunction: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = Split_strategy.t
module SplitGlobalStrategy: State_builder.Ref  with type data = Split_strategy.t
module ValShowProgress: Parameter_sig.Bool 
module ValShowPerf: Parameter_sig.Bool 
module ValPerfFlamegraphs: Parameter_sig.Filepath 
module ShowSlevel: Parameter_sig.Int 
module PrintCallstacks: Parameter_sig.Bool 
module ReportRedStatuses: Parameter_sig.Filepath 
module NumerorsLogFile: Parameter_sig.Filepath 
module MemExecAll: Parameter_sig.Bool 
module InterpreterMode: Parameter_sig.Bool 
module StopAtNthAlarm: Parameter_sig.Int 

Dynamic allocation

module AllocBuiltin: Parameter_sig.String 
module AllocFunctions: Parameter_sig.String_set 
module AllocReturnsNull: Parameter_sig.Bool 
module MallocLevel: Parameter_sig.Int 
module Precision: Parameter_sig.Int 

Meta-option

val configure_precision : unit -> unit
val parameters_correctness : Typed_parameter.t list
val parameters_tuning : Typed_parameter.t list
val dkey_initial_state : category

Debug categories responsible for printing initial and final states of Value. Enabled by default, but can be disabled via the command-line: -value-msg-key="-initial_state,-final_state"

val dkey_final_states : category
val dkey_summary : category
val wkey_alarm : warn_category

Warning category used when emitting an alarm in "warning" mode.

val wkey_locals_escaping : warn_category

Warning category used for the warning "locals escaping scope".

val wkey_garbled_mix : warn_category

Warning category used to print garbled mix

val wkey_builtins_missing_spec : warn_category

Warning category used for "cannot use builtin due to missing spec"

val wkey_builtins_override : warn_category

Warning category used for "definition overridden by builtin"

val wkey_libc_unsupported_spec : warn_category

Warning category used for calls to libc functions whose specification is currently unsupported.

val wkey_loop_unroll_auto : warn_category

Warning category used for "Automatic loop unrolling"

val wkey_loop_unroll_partial : warn_category

Warning category used for "loop not completely unrolled"

val wkey_missing_loop_unroll : warn_category

Warning category used to identify loops without unroll annotations

val wkey_missing_loop_unroll_for : warn_category

Warning category used to identify for loops without unroll annotations

val wkey_signed_overflow : warn_category

Warning category for signed overflows

val wkey_invalid_assigns : warn_category

Warning category for 'completely invalid' assigns clause

val wkey_experimental : warn_category

Warning category for experimental domains or features.

val wkey_unknown_size : warn_category

Warning category for 'size of type T cannot be computed'.

val dkey_pointer_comparison : category

Debug category used to print information about invalid pointer comparisons

val dkey_cvalue_domain : category

Debug category used to print the cvalue domain on Frama_C_dump|show_each functions.

val dkey_incompatible_states : category
val dkey_iterator : category

Debug category used to print information about the iteration

val dkey_callbacks : category

Debug category used when using Eva callbacks when recording the results of a function analysis.

val dkey_widening : category

Debug category used to print the usage of widenings.

val dkey_recursion : category

Debug category used to print messages about recursive calls.

val register_builtin : string -> unit

Registers available cvalue builtins for the -eva-builtin option.

val register_domain : name:string -> descr:string -> unit

Registers available domain names for the -eva-domains option.

val enabled_domains : unit -> (string * string) list

Returns the list (name, descr) of currently enabled domains.

val use_builtin : Cil_types.kernel_function -> string -> unit

use_builtin kf b adds a builtin override for function `kf` to builtin `b`.

val use_global_value_partitioning : Cil_types.varinfo -> unit

use_global_value_partitioning vi enable value partitioning on the global variable `vi`.