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 CvalueDomain: Parameter_sig.Bool 
module EqualityDomain: Parameter_sig.Bool 
module GaugesDomain: Parameter_sig.Bool 
module SymbolicLocsDomain: Parameter_sig.Bool 
module BitwiseOffsmDomain: Parameter_sig.Bool 
module InoutDomain: Parameter_sig.Bool 
module SignDomain: Parameter_sig.Bool 
module PrinterDomain: Parameter_sig.Bool 
module ApronOctagon: Parameter_sig.Bool 
module ApronBox: Parameter_sig.Bool 
module PolkaLoose: Parameter_sig.Bool 
module PolkaStrict: Parameter_sig.Bool 
module PolkaEqualities: Parameter_sig.Bool 
module EqualityCall: Parameter_sig.String 
module EqualityCallFunction: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = string
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 NoResultsAll: Parameter_sig.Bool 
module ResultsCallstack: Parameter_sig.Bool 
module JoinResults: Parameter_sig.Bool 
module WarnLeftShiftNegative: Parameter_sig.Bool 
module WarnSignedConvertedDowncast: Parameter_sig.Bool 
module WarnPointerSubstraction: Parameter_sig.Bool 
module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set 
module IgnoreRecursiveCalls: Parameter_sig.Bool 
module MemoryFootprint: 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 WideningLevel: Parameter_sig.Int 
module ArrayPrecisionLevel: Parameter_sig.Int 
module AllocatedContextValid: Parameter_sig.Bool 
module InitializationPaddingGlobals: Parameter_sig.String 
module SaveFunctionState: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = string
module LoadFunctionState: Parameter_sig.Map  with type key = Cil_types.kernel_function
                     and type value = string
val get_SaveFunctionState : unit -> Cil_types.kernel_function * string
val get_LoadFunctionState : unit -> Cil_types.kernel_function * 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 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 ValShowInitialState: Parameter_sig.Bool 
module ValShowPerf: Parameter_sig.Bool 
module ValPerfFlamegraphs: Parameter_sig.String 
module ShowSlevel: Parameter_sig.Int 
module PrintCallstacks: Parameter_sig.Bool 
module AlarmsWarnings: Parameter_sig.Bool 
module WarnBuiltinOverride: Parameter_sig.Bool 
module MemExecAll: Parameter_sig.Bool 
module InterpreterMode: Parameter_sig.Bool 
module ObviouslyTerminatesAll: Parameter_sig.Bool 
module ObviouslyTerminatesFunctions: Parameter_sig.Fundec_set 
module StopAtNthAlarm: Parameter_sig.Int 

Dynamic allocation

module MallocFunctions: Parameter_sig.String_set 
module AllocReturnsNull: Parameter_sig.Bool 
module MallocLevel: Parameter_sig.Int 
val parameters_correctness : Typed_parameter.t list
val parameters_tuning : Typed_parameter.t list
val parameters_abstractions : 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 wkey_alarm : warn_category

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

val dkey_garbled_mix : category

Debug category used to print garbled mix

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