Module Value_parameters

module Value_parameters: sig .. end

val kernel_parameters_correctness : Typed_parameter.t list

val parameters_correctness : Typed_parameter.t list

val parameters_tuning : Typed_parameter.t list

val add_dep : Typed_parameter.parameter -> unit

val add_correctness_dep : Typed_parameter.t -> unit

val add_precision_dep : Typed_parameter.t -> unit

module Fc_config: Config

include struct ... end

module ForceValues: WithOutput(sig

val option_name : string
val help : string
val output_by_default : bool
end)

val precision_tuning : Cmdline.Group.t

val initial_context : Cmdline.Group.t

val performance : Cmdline.Group.t

val interpreter : Cmdline.Group.t

val alarms : Cmdline.Group.t

module NoResultsFunctions: Fundec_set(sig

val option_name : string
val arg_name : string
val help : string
end)

module NoResultsAll: False(sig

val option_name : string
val help : string
end)

module ResultsAfter: Bool(sig

val option_name : string
val help : string
val default : bool
end)

module ResultsCallstack: Bool(sig

val option_name : string
val help : string
val default : bool
end)

module JoinResults: Bool(sig

val option_name : string
val help : string
val default : bool
end)

module MemoryFootprint: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module AllRoundingModes: False(sig

val option_name : string
val help : string
end)

module AllRoundingModesConstants: False(sig

val option_name : string
val help : string
end)

module UndefinedPointerComparisonPropagateAll: False(sig

val option_name : string
val help : string
end)

module WarnLeftShiftNegative: True(sig

val option_name : string
val help : string
end)

module LeftShiftNegativeOld: True(sig

val option_name : string
val help : string
end)

module WarnPointerSubstraction: True(sig

val option_name : string
val help : string
end)

module IgnoreRecursiveCalls: False(sig

val option_name : string
val help : string
end)

module WarnCopyIndeterminate: Kernel_function_set(sig

val option_name : string
val arg_name : string
val help : string
end)

module ShowTrace: False(sig

val option_name : string
val help : string
end)

module AutomaticContextMaxDepth: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module AutomaticContextMaxWidth: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module AllocatedContextValid: False(sig

val option_name : string
val help : string
end)

module InitializedPaddingGlobals: True(sig

val option_name : string
val help : string
end)

module WideningLevel: Int(sig

val default : int
val option_name : string
val arg_name : string
val help : string
end)

module ILevel: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module SemanticUnrollingLevel: Zero(sig

val option_name : string
val arg_name : string
val help : string
end)

module SlevelFunction: Kernel_function_map(sig
include Datatype.Int

type key = Cil_types.kernel_function 


val of_string : key:'a -> prev:'b -> string option -> int option
val to_string : key:'a -> int option -> string option
end)(sig

val option_name : string
val arg_name : string
val help : string
val default : 'a Kernel_function.Map.t
end)

module SlevelMergeAfterLoop: Kernel_function_set(sig

val option_name : string
val arg_name : string
val help : string
end)

module SplitReturnFunction: Kernel_function_map(sig
include Split_strategy

type key = Cil_types.kernel_function 


val of_string : key:key ->
       prev:t option -> string option -> split_strategy option
val to_string : key:'a -> split_strategy option -> string option
end)(sig

val option_name : string
val arg_name : string
val help : string
val default : 'a Kernel_function.Map.t
end)

module SplitReturnAuto: False(sig

val option_name : string
val help : string
end)

module BuiltinsOverrides: Kernel_function_map(sig
include Datatype.String

type key = Cil_types.kernel_function 


val of_string : key:Kernel_function.t -> prev:'a -> string option -> string option
val to_string : key:'a -> 'b -> 'b
end)(sig

val option_name : string
val arg_name : string
val help : string
val default : 'a Kernel_function.Map.t
end)

module Subdivide_float_in_expr: Zero(sig

val option_name : string
val arg_name : string
val help : string
end)

module UsePrototype: Kernel_function_set(sig

val option_name : string
val arg_name : string
val help : string
end)

module RmAssert: False(sig

val option_name : string
val help : string
end)

module MemExecAll: False(sig

val option_name : string
val help : string
end)

module ArrayPrecisionLevel: Int(sig

val default : int
val option_name : string
val arg_name : string
val help : string
end)

module SeparateStmtStart: String_set(sig

val option_name : string
val arg_name : string
val help : string
end)

module SeparateStmtWord: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module SeparateStmtOf: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module ValShowProgress: True(sig

val option_name : string
val help : string
end)

module ValShowInitialState: True(sig

val option_name : string
val help : string
end)

module TimingStep: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module FloatTimingStep: State_builder.Float_ref(sig

val default : unit -> float
val name : string
val dependencies : State.t list
end)

module ValShowPerf: False(sig

val option_name : string
val help : string
end)

module ShowSlevel: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module PrintCallstacks: False(sig

val option_name : string
val help : string
end)

module InterpreterMode: False(sig

val option_name : string
val help : string
end)

module ObviouslyTerminatesFunctions: Fundec_set(sig

val option_name : string
val arg_name : string
val help : string
end)

module ObviouslyTerminatesAll: False(sig

val option_name : string
val help : string
end)

module StopAtNthAlarm: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

module InitialStateChanged: Int(sig

val option_name : string
val default : int
val arg_name : string
val help : string
end)

val parameters_correctness : Typed_parameter.t list

val parameters_tuning : Typed_parameter.t list