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 EqualityStorage:Parameter_sig.Bool
module SymbolicLocsStorage:Parameter_sig.Bool
module GaugesStorage:Parameter_sig.Bool
module ApronStorage:Parameter_sig.Bool
module BitwiseOffsmStorage:Parameter_sig.Bool
module AutomaticContextMaxDepth:Parameter_sig.Int
module AutomaticContextMaxWidth:Parameter_sig.Int
module AllRoundingModesConstants:Parameter_sig.Bool
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 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 : 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 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`.