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/AutoSoundConfig/index.html

Module Goblint_lib.AutoSoundConfig

Automatically turning on analyses required to ensure soundness based on a given specification (e.g., SV-COMP specification) or programming idioms (e.g., longjmp) in the analyzed code, but only when it is possible to do so automatically. This does not fully exempt from the need for manual configuration.

val enableSpecAnalyses : SvcompSpec.t -> string list -> unit
val enableOptions : string list -> unit
val enableAnalysesForMemSafetySpecification : unit -> unit
val enableAnalysesForTerminationSpecification : unit -> unit
val enableAnalysesForSpecification : unit -> unit
val longjmpAnalyses : string list
val activateLongjmpAnalysesWhenRequired : unit -> unit