Module `Goblint_lib.AutoTune`Source

Sourcemodule FunctionSet : sig ... end

Sourcemodule FunctionCallMap : sig ... end

val addOrCreateMap : 
  FunctionSet.elt ->
  (FunctionSet.t * int) option ->
  (FunctionSet.t * int) option

Source

class collectFunctionCallsVisitor : (FunctionSet.t ref
    * (FunctionSet.t * int) FunctionCallMap.t ref
    * GoblintCil.exp list FunctionCallMap.t ref
    * FunctionSet.elt) -> object ... end

Source

class functionVisitor : (FunctionSet.t FunctionCallMap.t ref
    * (FunctionSet.t * int) FunctionCallMap.t ref
    * GoblintCil.exp list FunctionCallMap.t ref) -> object ... end

Source

val functionCallMaps : 
  (FunctionSet.t FunctionCallMap.t
   * (FunctionSet.t * int) FunctionCallMap.t
   * GoblintCil.exp list FunctionCallMap.t)
    ResettableLazy.t

Sourceval calledFunctions : FunctionCallMap.key -> FunctionSet.t

Sourceval callingFunctions : FunctionCallMap.key -> FunctionSet.t

Sourceval timesCalled : FunctionCallMap.key -> int

Sourceval functionArgs : FunctionCallMap.key -> GoblintCil.exp list option

Sourceval findMallocWrappers : unit -> unit

Sourceval isExtern : GoblintCil.storage -> bool

Source

val setCongruenceRecursive : 
  GoblintCil.fundec ->
  int ->
  (GoblintCil.varinfo -> FunctionSet.t) ->
  unit

Sourceexception ModFound

Sourceclass modVisitor : object ... end

Sourceclass modFunctionAnnotatorVisitor : object ... end

Sourceval addModAttributes : GoblintCil.file -> unit

Sourceval disableIntervalContextsInRecursiveFunctions : unit -> unit

Sourceval notNeccessaryThreadAnalyses : string list

Sourceval reduceThreadAnalyses : unit -> unit

Sourceval focusOnSpecification : unit -> unit

Sourceexception EnumFound

Sourceclass enumVisitor : object ... end

Sourceval hasEnums : GoblintCil.file -> bool

Sourceclass addTypeAttributeVisitor : object ... end

Sourceval selectArrayDomains : GoblintCil.file -> unit

Sourcetype option = {

value : int;
cost : int;
activate : unit -> unit;

}

Sourcemodule VariableMap : sig ... end

Sourcemodule VariableSet : sig ... end

Sourceval isComparison : GoblintCil.binop -> bool

Sourceval extractVar : GoblintCil.exp -> GoblintCil.varinfo option

Source

val extractOctagonVars : 
  GoblintCil.exp ->
  [> `Left of GoblintCil.varinfo * GoblintCil.varinfo
  | `Right of GoblintCil.varinfo ]
    option

Source

val addOrCreateVarMapping : 
  int VariableMap.t ref ->
  GoblintCil.varinfo ->
  int ->
  bool ->
  unit

Source

val handle : 
  int VariableMap.t ref ->
  int ->
  bool ->
  [< `Left of GoblintCil.varinfo * GoblintCil.varinfo
  | `Right of GoblintCil.varinfo ]
    option ->
  unit

Sourceclass octagonVariableVisitor : (int VariableMap.t ref * bool) -> object ... end

Sourceval topVars : int -> 'a VariableMap.t -> VariableMap.key list

Sourceclass octagonFunctionVisitor : (VariableMap.key list list ref * int) -> object ... end

Sourceval congruenceOption : AutoTune0.complexityFactors -> 'a -> option

Source

val apronOctagonOption : 
  AutoTune0.complexityFactors ->
  GoblintCil.file ->
  option

Sourceval wideningOption : AutoTune0.complexityFactors -> 'a -> option

Sourceval estimateComplexity : AutoTune0.complexityFactors -> 'a -> int

Sourceval totalTarget : int

Sourceval chooseFromOptions : int -> option list -> option list

Sourceval isActivated : string -> bool

Sourceval chooseConfig : GoblintCil.file -> unit

Sourceval reset_lazy : unit -> unit

package goblint

Module Goblint_lib.AutoTuneSource

Module `Goblint_lib.AutoTune`Source