Module Goblint_lib.AutoTune

Autotuning of the configuration based on syntactic heuristics.

module FunctionSet : sig ... end
module FunctionCallMap : sig ... end
val addOrCreateMap : FunctionSet.elt -> (FunctionSet.t * int) option -> (FunctionSet.t * int) option
class collectFunctionCallsVisitor : (FunctionSet.t Stdlib.ref * (FunctionSet.t * int) FunctionCallMap.t Stdlib.ref * GoblintCil.exp list FunctionCallMap.t Stdlib.ref * FunctionSet.elt) -> object ... end
class functionVisitor : (FunctionSet.t FunctionCallMap.t Stdlib.ref * (FunctionSet.t * int) FunctionCallMap.t Stdlib.ref * GoblintCil.exp list FunctionCallMap.t Stdlib.ref * FunctionSet.t Stdlib.ref) -> object ... end
exception Found
class findAllocsInLoops : object ... end
type functionCallMaps = {
  1. calling : FunctionSet.t FunctionCallMap.t;
  2. calledBy : (FunctionSet.t * int) FunctionCallMap.t;
  3. argLists : GoblintCil.Cil.exp list FunctionCallMap.t;
  4. dynamicallyCalled : FunctionSet.t;
}
val functionCallMaps : functionCallMaps ResettableLazy.t
val calledFunctions : FunctionCallMap.key -> FunctionSet.t
val callingFunctions : FunctionCallMap.key -> FunctionSet.t
val timesCalled : FunctionCallMap.key -> int
val functionArgs : FunctionCallMap.key -> GoblintCil.Cil.exp list option
val findMallocWrappers : unit -> unit
val isExtern : GoblintCil.storage -> bool
val setCongruenceRecursive : GoblintCil.fundec -> int -> (GoblintCil.varinfo -> FunctionSet.t) -> unit
exception ModFound
class modVisitor : object ... end
class modFunctionAnnotatorVisitor : object ... end
val addModAttributes : GoblintCil.file -> unit
val disableIntervalContextsInRecursiveFunctions : unit -> unit
val hasFunction : (LibraryDesc.t -> GoblintCil.Cil.exp list -> bool) -> bool
val disableAnalyses : string -> string list -> unit
val enableAnalyses : string -> string -> string list -> unit
val notNeccessaryRaceAnalyses : string list
val notNeccessaryThreadAnalyses : string list
val hasSpec : SvcompSpec.t -> bool
val reduceAnalyses : unit -> unit
val focusOnMemSafetySpecification : unit -> unit
val focusOnTermination : unit -> unit
val focusOnConcurrencySafety : unit -> unit
val focusOnNoOverflows : unit -> unit
exception EnumFound
class enumVisitor : object ... end
val hasEnums : GoblintCil.file -> bool
class addTypeAttributeVisitor : object ... end
val selectArrayDomains : GoblintCil.file -> unit
type option = {
  1. value : int;
  2. cost : int;
  3. activate : unit -> unit;
}
module VariableMap : sig ... end
module VariableSet : sig ... end
module OctagonTracked = RelationCil.AutotuneTracked
val isComparison : GoblintCil.binop -> bool
val extractVar : GoblintCil.exp -> GoblintCil.varinfo option
val extractBinOpVars : GoblintCil.exp -> GoblintCil.exp -> GoblintCil.varinfo list
val extractOctagonVars : GoblintCil.exp -> GoblintCil.varinfo list
val addOrCreateVarMapping : int VariableMap.t Stdlib.ref -> GoblintCil.varinfo -> int -> bool -> unit
class octagonVariableVisitor : (int VariableMap.t Stdlib.ref * bool) -> object ... end
val topVars : int -> 'a VariableMap.t -> VariableMap.key list
class octagonFunctionVisitor : (VariableMap.key list list Stdlib.ref * int) -> object ... end
val congruenceOption : Goblint_lib__.AutoTune0.complexityFactors -> 'a -> option
val apronOctagonOption : Goblint_lib__.AutoTune0.complexityFactors -> GoblintCil.file -> option
val wideningOption : Goblint_lib__.AutoTune0.complexityFactors -> 'a -> option
val activateTmpSpecialAnalysis : unit -> unit
val estimateComplexity : Goblint_lib__.AutoTune0.complexityFactors -> 'a -> int
val totalTarget : int
val chooseFromOptions : int -> option list -> option list
val isActivated : string -> bool
val isTerminationTask : unit -> bool
val chooseConfig : GoblintCil.file -> unit
val reset_lazy : unit -> unit