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
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
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