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 (9)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.1.0.tbz
sha256=bfc412ec2e447eaef6f4f83892e3511ebf305593cb00561c1406be3ae8bf48e9
sha512=5f2a162e5f36bffafc9836b0d18b5b2808cecfa6bf68f83bb7d1e8b9947ac74cf07776eb09274b4b29d55c897a45a10768f0d9ed25810cf6ba2409c525e4cd4d

doc/goblint.lib/Goblint_lib/index.html

Module Goblint_libSource

module AbortUnless : sig ... end

An analysis checking whether a function only returns if its only argument has a non-zero value.

module AbstractionDomainProperties : sig ... end
module Access : sig ... end
module AccessAnalysis : sig ... end

Access analysis.

module AccessDomain : sig ... end
module AccessKind : sig ... end
module AddressDomain : sig ... end
module AfterConfig : sig ... end
module Analyses : sig ... end

Signatures for analyzers, analysis specifications, and result output.

Sourcemodule ApronAnalysis : sig ... end
Sourcemodule ApronDomain : sig ... end
Sourcemodule ApronPrecCompareUtil : sig ... end
Sourcemodule ApronPriv : sig ... end
module ArrayDomain : sig ... end
module Assert : sig ... end
Sourcemodule AutoTune : sig ... end
Sourcemodule AutoTune0 : sig ... end
module Base : sig ... end

Value analysis.

module BaseDomain : sig ... end

domain of the base analysis

module BasePriv : sig ... end
module BaseUtil : sig ... end
module Basetype : sig ... end
module BoolDomain : sig ... end
module CfgTools : sig ... end
module CilCfg : sig ... end
module CilLval : sig ... end
module CilMaps : sig ... end
module CilType : sig ... end
module Cilfacade : sig ... end

Helpful functions for dealing with Cil.

module Cilfacade0 : sig ... end
module CommonPriv : sig ... end
module CompareAST : sig ... end
module CompareCFG : sig ... end
module CompareCIL : sig ... end
module CompilationDatabase : sig ... end
module ConcDomain : sig ... end
module CondVars : sig ... end

Must equality between variables and logical expressions.

Sourcemodule ConfigProfile : sig ... end
Sourcemodule ConfigVersion : sig ... end
module Constants : sig ... end
module Constraints : sig ... end

How to generate constraints for a solver using specifications described in Analyses.

module ContextUtil : sig ... end

Definition of Goblint specific user defined C attributes and their alternatives via options *

module Control : sig ... end

An analyzer that takes the CFG from MyCFG, a solver from Selector, constraints from Constraints (using the specification from MCP)

module Deadlock : sig ... end

Deadlock analysis.

module DeadlockDomain : sig ... end
module DisjointDomain : sig ... end

Abstract domains for collections of elements from disjoint unions of domains. Formally, the elements form a cofibered domain from a discrete category.

module DomainProperties : sig ... end
module Edge : sig ... end
module EffectWConEq : sig ... end
module EscapeDomain : sig ... end
module EvalAssert : sig ... end

Instruments a program by inserting asserts either:

module Events : sig ... end
module ExpRelation : sig ... end

An analysis specification to answer questions about how two expressions relate to each other.

module ExpressionEvaluation : sig ... end
module Expsplit : sig ... end
module ExtractPthread : sig ... end

Tracking of pthread lib code. Output to promela.

module FileDomain : sig ... end
module FileUse : sig ... end

An analysis for checking correct use of file handles.

module FlagHelper : sig ... end
module FlagModeDomain : sig ... end
module FloatDomain : sig ... end
module FloatOps : sig ... end
module Generic : sig ... end
module GobConfig : sig ... end

New, untyped, path-based configuration subsystem.

module GobFormat : sig ... end
module GobFpath : sig ... end
module GobHashtbl : sig ... end
module GobList : sig ... end
module GobOption : sig ... end
module GobResult : sig ... end
module GobSys : sig ... end
module GobUnix : sig ... end
module GobYaml : sig ... end
module GobYojson : sig ... end
module GoblintDir : sig ... end
module Goblintutil : sig ... end

Globally accessible flags and utility functions.

module Graphml : sig ... end
module HoareDomain : sig ... end

Abstract domains with Hoare ordering.

module IntDomain : sig ... end
module IntDomainProperties : sig ... end
module IntOps : sig ... end
module Invariant : sig ... end
module InvariantCil : sig ... end
module JsonSchema : sig ... end
module Lattice : sig ... end

The lattice signature and simple functors for building lattices.

module LazyEval : sig ... end
module LibraryDesc : sig ... end
module LibraryDsl : sig ... end

Library function descriptor DSL.

module LibraryFunctionEffects : sig ... end
module LibraryFunctions : sig ... end
module LockDomain : sig ... end
module LocksetAnalysis : sig ... end

Basic lockset analyses.

module LoopUnrolling : sig ... end
module Lval : sig ... end
module LvalMapDomain : sig ... end
module MCP : sig ... end

Master Control Program

module MCPAccess : sig ... end
module MCPRegistry : sig ... end
module MHP : sig ... end
module MHPAnalysis : sig ... end
Sourcemodule Maingoblint : sig ... end

This is the main program!

module MakefileUtil : sig ... end
module MallocFresh : sig ... end
module MallocWrapperAnalysis : sig ... end

An analysis that handles the case when malloc is called from a wrapper function all over the code.

module Malloc_null : sig ... end

Path-sensitive analysis that verifies checking the result of the malloc function.

module MapDomain : sig ... end

Specification and functors for maps.

module MaxIdUtil : sig ... end
module MayLocks : sig ... end

May lockset analysis (unused).

module MessageCategory : sig ... end
module MessageUtil : sig ... end
module Messages : sig ... end
module MusteqDomain : sig ... end
module MutexAnalysis : sig ... end

Protecting mutex analysis. Must locksets locally and for globals.

module MutexEventsAnalysis : sig ... end

Mutex events analysis (Lock and Unlock).

module MyARG : sig ... end
module MyCFG : sig ... end

Our Control-flow graph implementation.

module MyCheck : sig ... end
module Node : sig ... end
module Node0 : sig ... end

Node functions to avoid dependency cycles.

module ObserverAnalysis : sig ... end
module ObserverAutomaton : sig ... end
module Options : sig ... end
module PartitionDomain : sig ... end

Partitioning domains.

module PostSolver : sig ... end
module PreValueDomain : sig ... end
module PrecCompare : sig ... end
module PrecCompareUtil : sig ... end
module PrecisionUtil : sig ... end
Sourcemodule Prelude : sig ... end
module Preprocessor : sig ... end
module Printable : sig ... end

Some things are not quite lattices ...

module PrivPrecCompareUtil : sig ... end
module ProcessPool : sig ... end
module PthreadDomain : sig ... end
module PthreadSignals : sig ... end

Analysis of must-received pthread_signals.

module Queries : sig ... end

Structures for the querying subsystem.

module RaceAnalysis : sig ... end

Data race analysis.

module Refinement : sig ... end
module Region : sig ... end

Assigning static regions to dynamic memory.

module RegionDomain : sig ... end
module ResettableLazy : sig ... end
module RichVarinfo : sig ... end
module SLR : sig ... end

The 'slr*' solvers.

module SLRphased : sig ... end
module SLRterm : sig ... end
module Sarif : sig ... end
module SarifRules : sig ... end
module SarifType : sig ... end
module Selector : sig ... end
module Serialize : sig ... end
module Server : sig ... end
module SetDomain : sig ... end
module Signs : sig ... end

An analysis specification for didactic purposes.

module Spec : sig ... end

Analysis by specification file.

module SpecCore : sig ... end
module SpecDomain : sig ... end
module SpecLexer : sig ... end
module SpecParser : sig ... end
module SpecUtil : sig ... end
module StackDomain : sig ... end
module StackTrace : sig ... end

Stack-trace "analyses".

module StructDomain : sig ... end

Abstract domains representing structs.

module Svcomp : sig ... end
module SvcompSpec : sig ... end
module SymbLocks : sig ... end

Symbolic lock-sets for use in per-element patterns.

module SymbLocksDomain : sig ... end
module Taint : sig ... end

An analysis specification for didactic purposes.

module Td3 : sig ... end

Incremental terminating top down solver that optionally only keeps values at widening points and restores other values afterwards.

module Termination : sig ... end

Termination of loops.

module ThreadAnalysis : sig ... end

Thread creation and uniqueness analyses.

module ThreadEscape : sig ... end

Variables that escape threads using the last argument from pthread_create.

module ThreadFlag : sig ... end

Multi-threadedness analysis.

module ThreadFlagDomain : sig ... end
module ThreadId : sig ... end

Current thread ID analysis.

module ThreadIdDomain : sig ... end
module ThreadJoins : sig ... end
module ThreadReturn : sig ... end

Thread returning analysis.

module TimeUtil : sig ... end
module Timeout : sig ... end
module Timing : sig ... end
module TopDown : sig ... end

Top down solver using box/warrow. This is superseded by td3 but kept as a simple version without term & space (& incremental).

module TopDown_deprecated : sig ... end
module TopDown_space_cache_term : sig ... end

Terminating top down solver that only keeps values at widening points and restores other values afterwards.

module TopDown_term : sig ... end

Top down solver.

module Tracing : sig ... end
module Transform : sig ... end
module Uninit : sig ... end

Local variable initialization analysis.

module UnionDomain : sig ... end
module UnitAnalysis : sig ... end

An analysis specification for didactic purposes.

module UpdateCil : sig ... end
module UpdateCil0 : sig ... end
module ValueDomain : sig ... end
module VarEq : sig ... end

Variable equalities necessary for per-element patterns.

module VarQuery : sig ... end
Sourcemodule Version : sig ... end
module Violation : sig ... end
Sourcemodule ViolationZ3 : sig ... end
module WideningThresholds : sig ... end
module Witness : sig ... end
module WitnessConstraints : sig ... end

An analysis specification for witnesses.

module WitnessUtil : sig ... end
module Worklist : sig ... end
module XmlUtil : sig ... end
module YamlWitness : sig ... end
module YamlWitnessType : sig ... end