package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (10)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. M
    Michael Petter
  7. A
    Ali Rasim Kocal
  8. R
    Ralf Vogler
  9. K
    Kalmer Apinis
  10. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.7.1.tbz
sha256=af01aac256229f33a90a9fcbfed04b01e3097f154d4d124f006476d6387c6a66
sha512=2a93bfe16881adbc2d8dcbfe38c1e19cd24ca105d8e1eda13d02440f3002874ffe2957dfd937510765233a054a40568b0052db92e31d382a5bd215d1ec12565c

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

Module Goblint_lib.AutoTuneSource

Autotuning of the configuration based on syntactic heuristics.

Sourcemodule FunctionSet : sig ... end
Sourcemodule FunctionCallMap : sig ... end
Sourceval addOrCreateMap : FunctionSet.elt -> (FunctionSet.t * int) option -> (FunctionSet.t * int) option
Sourceexception Found
Sourceclass findAllocsInLoops : object ... end
Sourcetype 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;
}
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
Sourceval 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.t -> GoblintCil.Cil.exp list -> bool) -> bool
Sourceval disableAnalyses : string -> string list -> unit
Sourceval enableAnalyses : string -> string -> string list -> unit
Sourceval notNeccessaryRaceAnalyses : string list
Sourceval notNeccessaryThreadAnalyses : string list
Sourceval hasSpec : SvcompSpec.t -> bool
Sourceval reduceAnalyses : unit -> unit
Sourceval focusOnMemSafetySpecification : unit -> unit
Sourceval focusOnTermination : unit -> unit
Sourceval focusOnConcurrencySafety : unit -> unit
Sourceval focusOnNoOverflows : unit -> unit
Sourceexception EnumFound
Sourceclass enumVisitor : object ... end
Sourceval hasEnums : GoblintCil.file -> bool
Sourceclass addTypeAttributeVisitor : object ... end
Sourceval selectArrayDomains : GoblintCil.file -> unit
Sourcetype option = {
  1. value : int;
  2. cost : int;
  3. activate : unit -> unit;
}
Sourcemodule VariableMap : sig ... end
Sourcemodule VariableSet : sig ... end
module OctagonTracked = RelationCil.AutotuneTracked
Sourceval isComparison : GoblintCil.binop -> bool
Sourceval extractVar : GoblintCil.exp -> GoblintCil.varinfo option
Sourceval extractBinOpVars : GoblintCil.exp -> GoblintCil.exp -> GoblintCil.varinfo list
Sourceval extractOctagonVars : GoblintCil.exp -> GoblintCil.varinfo list
Sourceval addOrCreateVarMapping : int VariableMap.t ref -> GoblintCil.varinfo -> int -> bool -> 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 : Goblint_lib__.AutoTune0.complexityFactors -> 'a -> option
Sourceval 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 chooseConfig : GoblintCil.file -> unit
Sourceval reset_lazy : unit -> unit