Module `Goblint_lib.AutoTune`Source

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

Source

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

Source

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

Sourcetype functionCallMaps = {

calling : FunctionSet.t FunctionCallMap.t;
calledBy : (FunctionSet.t * int) FunctionCallMap.t;
argLists : GoblintCil.Cil.exp list FunctionCallMap.t;
dynamicallyCalled : FunctionSet.t;

}

Sourceval functionCallMaps : functionCallMaps ResettableLazy.t

Sourceval calledFunctions : FunctionCallMap.key -> FunctionSet.t

Sourceval callingFunctions : FunctionCallMap.key -> FunctionSet.t

Sourceval timesCalled : FunctionCallMap.key -> int

Sourceval functionArgs : FunctionCallMap.key -> GoblintCil.Cil.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 hasFunction : (LibraryDesc.special -> bool) -> bool

Sourceval disableAnalyses : string list -> unit

Sourceval enableAnalyses : string list -> unit

Sourceval notNeccessaryThreadAnalyses : string list

Sourceval reduceThreadAnalyses : unit -> unit

Sourceval longjmpAnalyses : string list

Sourceval activateLongjmpAnalysesWhenRequired : unit -> unit

Sourceval focusOnMemSafetySpecification : unit -> unit

Sourceval focusOnTermination : 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;

}

module VariableMap : sig ... end

module VariableSet : sig ... end

Sourceval isComparison : GoblintCil.binop -> bool

Sourceval isGoblintStub : GoblintCil.varinfo -> 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 Stdlib.ref ->
  GoblintCil.varinfo ->
  int ->
  bool ->
  unit

Source

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

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

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

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

Source

val congruenceOption : 
  Goblint_lib__.AutoTune0.complexityFactors ->
  'a ->
  option

Source

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

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

Sourceval activateTmpSpecialAnalysis : unit -> unit

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

Sourceval totalTarget : int

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

Sourceval isActivated : string -> bool

Sourceval isTerminationTask : unit -> bool

Sourceval specificationIsActivated : unit -> bool

Sourceval specificationTerminationIsActivated : unit -> bool

Sourceval chooseConfig : GoblintCil.file -> unit

Sourceval reset_lazy : unit -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/AutoTune/index.html

Module `Goblint_lib.AutoTune`Source

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/AutoTune/index.html

Module Goblint_lib.AutoTuneSource

Module `Goblint_lib.AutoTune`Source