sig
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 :
sig
type key = string
type value = Domain_mode.function_mode
type t
val set : t -> unit
val add_set_hook : (t -> t -> unit) -> unit
val add_update_hook : (t -> t -> unit) -> unit
val get : unit -> t
val clear : unit -> unit
val is_default : unit -> bool
val get_default : unit -> t
val option_name : string
val print_help : Format.formatter -> unit
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
val equal : t -> t -> bool
val add_aliases :
?visible:bool -> ?deprecated:bool -> string list -> unit
val is_set : unit -> bool
val unsafe_set : t -> unit
val parameter : Typed_parameter.t
type elt = key * value list
val is_empty : unit -> bool
val iter : (elt -> unit) -> unit
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
val add : elt -> unit
module As_string : Parameter_sig.String
module Category :
sig
type elt = elt
type t = elt Parameter_category.t
val none : t
val default : unit -> t
val all : unit -> t
val set_default : t -> unit
val add :
string -> State.t list -> elt Parameter_category.accessor -> t
val enable_all :
State.t list -> elt Parameter_category.accessor -> t
val enable_all_as : t -> unit
end
val find : key -> value list
val mem : key -> bool
end
module EqualityCall : Parameter_sig.String
module EqualityCallFunction :
sig
type key = Cil_types.kernel_function
type value = string
type t
val set : t -> unit
val add_set_hook : (t -> t -> unit) -> unit
val add_update_hook : (t -> t -> unit) -> unit
val get : unit -> t
val clear : unit -> unit
val is_default : unit -> bool
val get_default : unit -> t
val option_name : string
val print_help : Format.formatter -> unit
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
val equal : t -> t -> bool
val add_aliases :
?visible:bool -> ?deprecated:bool -> string list -> unit
val is_set : unit -> bool
val unsafe_set : t -> unit
val parameter : Typed_parameter.t
type elt = key * value option
val is_empty : unit -> bool
val iter : (elt -> unit) -> unit
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
val add : elt -> unit
module As_string : Parameter_sig.String
module Category :
sig
type elt = elt
type t = elt Parameter_category.t
val none : t
val default : unit -> t
val all : unit -> t
val set_default : t -> unit
val add :
string -> State.t list -> elt Parameter_category.accessor -> t
val enable_all :
State.t list -> elt Parameter_category.accessor -> t
val enable_all_as : t -> unit
end
val find : key -> value
val mem : key -> bool
end
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 MultidimSegmentLimit : Parameter_sig.Int
module MultidimDisjunctiveInvariants : 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 :
sig
type key = Cil_types.kernel_function
type value = int
type t
val set : t -> unit
val add_set_hook : (t -> t -> unit) -> unit
val add_update_hook : (t -> t -> unit) -> unit
val get : unit -> t
val clear : unit -> unit
val is_default : unit -> bool
val get_default : unit -> t
val option_name : string
val print_help : Format.formatter -> unit
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
val equal : t -> t -> bool
val add_aliases :
?visible:bool -> ?deprecated:bool -> string list -> unit
val is_set : unit -> bool
val unsafe_set : t -> unit
val parameter : Typed_parameter.t
type elt = key * value option
val is_empty : unit -> bool
val iter : (elt -> unit) -> unit
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
val add : elt -> unit
module As_string : Parameter_sig.String
module Category :
sig
type elt = elt
type t = elt Parameter_category.t
val none : t
val default : unit -> t
val all : unit -> t
val set_default : t -> unit
val add :
string -> State.t list -> elt Parameter_category.accessor -> t
val enable_all :
State.t list -> elt Parameter_category.accessor -> t
val enable_all_as : t -> unit
end
val find : key -> value
val mem : key -> bool
end
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 :
sig
type key = Cil_types.kernel_function
type value = int
type t
val set : t -> unit
val add_set_hook : (t -> t -> unit) -> unit
val add_update_hook : (t -> t -> unit) -> unit
val get : unit -> t
val clear : unit -> unit
val is_default : unit -> bool
val get_default : unit -> t
val option_name : string
val print_help : Format.formatter -> unit
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
val equal : t -> t -> bool
val add_aliases :
?visible:bool -> ?deprecated:bool -> string list -> unit
val is_set : unit -> bool
val unsafe_set : t -> unit
val parameter : Typed_parameter.t
type elt = key * value option
val is_empty : unit -> bool
val iter : (elt -> unit) -> unit
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
val add : elt -> unit
module As_string : Parameter_sig.String
module Category :
sig
type elt = elt
type t = elt Parameter_category.t
val none : t
val default : unit -> t
val all : unit -> t
val set_default : t -> unit
val add :
string -> State.t list -> elt Parameter_category.accessor -> t
val enable_all :
State.t list -> elt Parameter_category.accessor -> t
val enable_all_as : t -> unit
end
val find : key -> value
val mem : key -> bool
end
module BuiltinsOverrides :
sig
type key = Cil_types.kernel_function
type value = string
type t
val set : t -> unit
val add_set_hook : (t -> t -> unit) -> unit
val add_update_hook : (t -> t -> unit) -> unit
val get : unit -> t
val clear : unit -> unit
val is_default : unit -> bool
val get_default : unit -> t
val option_name : string
val print_help : Format.formatter -> unit
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
val equal : t -> t -> bool
val add_aliases :
?visible:bool -> ?deprecated:bool -> string list -> unit
val is_set : unit -> bool
val unsafe_set : t -> unit
val parameter : Typed_parameter.t
type elt = key * value option
val is_empty : unit -> bool
val iter : (elt -> unit) -> unit
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
val add : elt -> unit
module As_string : Parameter_sig.String
module Category :
sig
type elt = elt
type t = elt Parameter_category.t
val none : t
val default : unit -> t
val all : unit -> t
val set_default : t -> unit
val add :
string -> State.t list -> elt Parameter_category.accessor -> t
val enable_all :
State.t list -> elt Parameter_category.accessor -> t
val enable_all_as : t -> unit
end
val find : key -> value
val mem : key -> bool
end
module BuiltinsAuto : Parameter_sig.Bool
module BuiltinsList : Parameter_sig.Bool
module SplitReturnFunction :
sig
type key = Cil_types.kernel_function
type value = Split_strategy.t
type t
val set : t -> unit
val add_set_hook : (t -> t -> unit) -> unit
val add_update_hook : (t -> t -> unit) -> unit
val get : unit -> t
val clear : unit -> unit
val is_default : unit -> bool
val get_default : unit -> t
val option_name : string
val print_help : Format.formatter -> unit
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
val equal : t -> t -> bool
val add_aliases :
?visible:bool -> ?deprecated:bool -> string list -> unit
val is_set : unit -> bool
val unsafe_set : t -> unit
val parameter : Typed_parameter.t
type elt = key * value option
val is_empty : unit -> bool
val iter : (elt -> unit) -> unit
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
val add : elt -> unit
module As_string : Parameter_sig.String
module Category :
sig
type elt = elt
type t = elt Parameter_category.t
val none : t
val default : unit -> t
val all : unit -> t
val set_default : t -> unit
val add :
string -> State.t list -> elt Parameter_category.accessor -> t
val enable_all :
State.t list -> elt Parameter_category.accessor -> t
val enable_all_as : t -> unit
end
val find : key -> value
val mem : key -> bool
end
module SplitGlobalStrategy :
sig
val self : State.t
val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit
val is_computed : ?project:Project.t -> unit -> bool
module Datatype : Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
type data = Split_strategy.t
val set : data -> unit
val get : unit -> data
val clear : unit -> unit
end
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
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
val configure_precision : unit -> unit
val parameters_correctness : Typed_parameter.t list
val parameters_tuning : Typed_parameter.t list
val register_builtin : string -> unit
val register_domain : name:string -> descr:string -> unit
val enabled_domains : unit -> (string * string) list
val use_builtin : Cil_types.kernel_function -> string -> unit
val use_global_value_partitioning : Cil_types.varinfo -> unit
end