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.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

doc/goblint.lib/Goblint_lib/index.html

Module Goblint_libSource

Main library.

Framework

Sourcemodule Maingoblint : sig ... end

Main external executable functionality: command-line, front-end and analysis execution.

module Control : sig ... end

Main internal functionality: analysis of the program by abstract interpretation via constraint solving.

module Server : sig ... end

Interactive server mode using JSON-RPC.

CFG

Control-flow graphs (CFGs) are used to represent each function.

module Node = Node
module Edge = Edge
module MyCFG = MyCFG
module CfgTools : sig ... end

Construction and output of CFGs.

Specification

Analyses are specified by domains and transfer functions. A dynamic composition of analyses is combined with CFGs to produce a constraint system.

module Analyses : sig ... end

Analysis specification and constraint system signatures.

module Constraints : sig ... end

Construction of a constraint system from an analysis specification and CFGs. Transformatons of analysis specifications as functors.

module AnalysisState = AnalysisState
module AnalysisStateUtil : sig ... end
module ControlSpecC = ControlSpecC

Master control program (MCP) is the analysis specification for the dynamic product of activated analyses.

module MCP : sig ... end

MCP analysis specification.

module MCPRegistry : sig ... end

Registry of dynamically activatable analyses. Analysis specification modules for the dynamic product.

module MCPAccess : sig ... end

Memory access metadata module for MCP.

MCP allows activated analyses to query each other during the analysis. Query results from different analyses for the same query are met for precision.

module Queries : sig ... end

Queries and their result lattices.

MCP allows activated analyses to emit events to each other during the analysis.

module Events : sig ... end

Events.

Results

The following modules help query the constraint system solution using semantic information.

module ResultQuery : sig ... end

Perform queries on the constraint system solution.

module VarQuery : sig ... end

Queries for constraint variables related to semantic elements.

Configuration

Runtime configuration is represented as JSON. Options are specified and documented by the JSON schema src/common/util/options.schema.json.

module GobConfig = GobConfig
module AfterConfig = AfterConfig
Sourcemodule AutoTune : sig ... end

Autotuning of the configuration based on syntactic heuristics.

module JsonSchema = JsonSchema
module Options = Options

Analyses

Analyses activatable under MCP.

Value

Analyses related to values of program variables.

module Base : sig ... end

Non-relational value analysis aka base analysis (base).

Sourcemodule RelationAnalysis : sig ... end
Sourcemodule ApronAnalysis : sig ... end
Sourcemodule AffineEqualityAnalysis : sig ... end
module VarEq : sig ... end

Symbolic expression equalities analysis (var_eq).

module CondVars : sig ... end

Symbolic variable - logical expression equalities analysis (condvars).

module TmpSpecial : sig ... end

Analysis that tracks which variables hold the results of calls to math library functions (tmpSpecial).

Heap

Analyses related to the heap.

module Region : sig ... end

Analysis of disjoint heap regions for dynamically allocated memory (region).

module MallocFresh : sig ... end

Analysis of unescaped (i.e. thread-local) heap locations (mallocFresh).

module Malloc_null : sig ... end

Path-sensitive analysis of failed dynamic memory allocations (malloc_null).

module MemLeak : sig ... end

An analysis for the detection of memory leaks (memLeak).

module UseAfterFree : sig ... end

An analysis for the detection of use-after-free vulnerabilities (useAfterFree).

module MemOutOfBounds : sig ... end

An analysis for the detection of out-of-bounds memory accesses (memOutOfBounds).

Concurrency

Analyses related to concurrency.

Locks

Analyses related to locking.

module MutexEventsAnalysis : sig ... end

Mutex locking and unlocking analysis (mutexEvents).

module LocksetAnalysis : sig ... end

Basic lockset analyses.

module MutexTypeAnalysis : sig ... end

An analysis tracking the type of a mutex (pthreadMutexType).

module MutexAnalysis : sig ... end

Must lockset and protecting lockset analysis (mutex).

module MayLocks : sig ... end

May lockset analysis and analysis of double locking (maylocks).

module SymbLocks : sig ... end

Symbolic lockset analysis for per-element (field or index) locking patterns (symb_locks).

module Deadlock : sig ... end

Deadlock analysis (deadlock).

Threads

Analyses related to threads.

module ThreadFlag : sig ... end

Multi-threadedness analysis (threadflag).

module ThreadId : sig ... end

Current thread ID analysis (threadid).

module ThreadAnalysis : sig ... end

Created threads and their uniqueness analysis (thread).

module ThreadJoins : sig ... end

Joined threads analysis (threadJoins).

module MHPAnalysis : sig ... end

May-happen-in-parallel (MHP) analysis for memory accesses (mhp).

module ThreadReturn : sig ... end

Thread returning analysis which abstracts a thread's call stack by a boolean, indicating whether it is at the topmost call stack frame or not (threadreturn).

Other

module RaceAnalysis : sig ... end

Data race analysis (race).

module BasePriv : sig ... end

Non-relational thread-modular value analyses for Base.

Sourcemodule RelationPriv : sig ... end
module ThreadEscape : sig ... end

Escape analysis for thread-local variables (escape).

module PthreadSignals : sig ... end

Must received signals analysis for Pthread condition variables (pthreadSignals).

module ExtractPthread : sig ... end

Promela extraction analysis for Pthread programs (extract-pthread).

Longjmp

Analyses related to longjmp and setjmp.

module ActiveSetjmp : sig ... end

Analysis of active setjmp buffers (activeSetjmp).

module ModifiedSinceLongjmp : sig ... end

Analysis of variables modified since setjmp (modifiedSinceLongjmp).

module ActiveLongjmp : sig ... end

Analysis of active longjmp targets (activeLongjmp).

module PoisonVariables : sig ... end

Taint analysis of variables that were modified between setjmp and longjmp and not yet overwritten. (poisonVariables).

module Vla : sig ... end

Analysis of variable-length arrays (VLAs) in scope (vla).

Tutorial

Analyses for didactic purposes.

module Constants : sig ... end

Simple intraprocedural integer constants analysis example (constants).

module Signs : sig ... end

Simple intraprocedural integer signs analysis template (signs).

module Taint : sig ... end

Simple interprocedural taint analysis template (taint).

module UnitAnalysis : sig ... end

Simplest possible analysis with unit domain (unit).

Other

module Assert : sig ... end

Analysis of assert results (assert).

module FileUse : sig ... end

Analysis of correct file handle usage (file).

module LoopTermination : sig ... end

Termination analysis for loops and goto statements (termination).

module Uninit : sig ... end

Analysis of initialized local variables (uninit).

module Expsplit : sig ... end

Path-sensitive analysis according to values of arbitrary given expressions (expsplit).

module StackTrace : sig ... end

Call stack analyses (stack_trace, stack_trace_set, stack_loc).

module Spec : sig ... end

Analysis using finite automaton specification file (spec).

Helper

Analyses which only support other analyses.

module AccessAnalysis : sig ... end

Analysis of memory accesses (access).

module WrapperFunctionAnalysis : sig ... end

Family of analyses which provide symbolic locations for special library functions. Provides symbolic heap locations for dynamic memory allocations and symbolic thread identifiers for thread creation (mallocWrapper, threadCreateWrapper).

module TaintPartialContexts : sig ... end

Taint analysis of variables modified in a function (taintPartialContexts).

module UnassumeAnalysis : sig ... end

Unassume analysis (unassume).

module ExpRelation : sig ... end

Stateless symbolic comparison expression analysis (expRelation).

module AbortUnless : sig ... end

Analysis of assume_abort_if_not-style functions (abortUnless).

Domains

Domains used by analysis specifications and constraint systems are lattices.

Besides lattice operations, their elements can also be compared and output (in various formats). Those operations are specified by Printable.S.

module Printable = Printable
module Lattice = Lattice

General

Standard general-purpose domains and domain functors.

module BoolDomain : sig ... end

Boolean domains.

module SetDomain : sig ... end

Set domains.

module MapDomain : sig ... end

Map domains.

module TrieDomain : sig ... end

Trie domains.

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 HoareDomain : sig ... end

Abstract domains with Hoare ordering.

module PartitionDomain : sig ... end

Partitioning domains.

module FlagHelper : sig ... end

Domain alternatives chosen by a runtime flag.

Analysis-specific

Domains for specific analyses.

Value

Non-relational

Domains for Base analysis.

Numeric
module IntDomain : sig ... end

Abstract domains for C integers.

module FloatDomain : sig ... end

Abstract domains for C floating-point numbers.

Addresses

Memory locations are identified by mvalues, which consist of a variable and an offset. Mvalues are used throughout Goblint, not just the Base analysis.

Addresses extend mvalues with NULL, unknown pointers and string literals.

module Mval : sig ... end

Domains for mvalues: simplified lvalues, which start with a GoblintCil.varinfo. Mvalues are the result of resolving pointer dereferences in lvalues.

module Offset : sig ... end

Domains for variable offsets, i.e. array indices and struct fields.

module AddressDomain : sig ... end

Domains for addresses/pointers.

Complex
module StructDomain : sig ... end

Abstract domains for C structs.

module UnionDomain : sig ... end

Abstract domains for C unions.

module ArrayDomain : sig ... end

Abstract domains for C arrays.

module JmpBufDomain : sig ... end

Domains for setjmp and longjmp analyses, and setjmp buffers.

Combined

These combine the above domains together for Base analysis.

module BaseDomain : sig ... end

Full domain of Base analysis.

module ValueDomain : sig ... end

Domain for a single Base analysis value.

module ValueDomainQueries : sig ... end

Queries within ValueDomain.

Relational

Domains for RelationAnalysis.

Sourcemodule RelationDomain : sig ... end
Sourcemodule ApronDomain : sig ... end
Sourcemodule AffineEqualityDomain : sig ... end

Concurrency

module MutexAttrDomain : sig ... end

Mutex attribute type domain.

module LockDomain : sig ... end

Lockset domains.

module SymbLocksDomain : sig ... end

Symbolic lockset domain.

module DeadlockDomain : sig ... end

Deadlock domain.

module ThreadFlagDomain : sig ... end

Multi-threadedness flag domains.

module ThreadIdDomain : sig ... end

Thread ID domains.

module ConcDomain : sig ... end

Domains for thread sets and their uniqueness.

module MHP : sig ... end

May-happen-in-parallel (MHP) domain.

module EscapeDomain : sig ... end

Domain for escaped thread-local variables.

module PthreadDomain : sig ... end

Domains for extraction of Pthread programs.

Other

module Basetype = Basetype
module Lval : sig ... end

Domains for GoblintCil.lval.

module Access : sig ... end

Memory accesses and their manipulation.

module AccessDomain : sig ... end

Domain for memory accesses.

module MusteqDomain : sig ... end

Symbolic lvalue equalities domain.

module RegionDomain : sig ... end

Domains for disjoint heap regions.

module FileDomain : sig ... end

Domains for file handles.

module StackDomain : sig ... end

Call stack domains.

module MvalMapDomain : sig ... end

Domains for mvalue maps.

module SpecDomain : sig ... end

Domains for finite automaton specification file analysis.

Testing

Modules related to (property-based) testing of domains.

module DomainProperties : sig ... end

QCheck properties for lattice properties.

module AbstractionDomainProperties : sig ... end

QCheck properties for abstract operations.

module IntDomainProperties : sig ... end

QCheck properties for IntDomain.

Incremental

Incremental analysis is for analyzing multiple versions of the same program and reusing as many results as possible.

module CompareCIL : sig ... end

Comparison of CIL files.

module CompareAST : sig ... end

Comparison of CIL ASTs.

module CompareCFG : sig ... end

Comparison of CFGs.

module UpdateCil : sig ... end

Combination of CIL files using comparison results.

module MaxIdUtil : sig ... end

Tracking of maximum CIL IDs in use.

module Serialize : sig ... end

Serialization/deserialization of incremental analysis data.

module CilMaps : sig ... end

Special maps used for incremental comparison.

Solvers

Generic solvers are used to solve (side-effecting) constraint systems.

Top-down

The top-down solver family.

module Td3 : sig ... end

Incremental/interactive terminating top-down solver, which supports space-efficiency and caching (td3).

module TopDown : sig ... end

Warrowing top-down solver (topdown). Simpler version of Td3 without terminating, space-efficiency and incremental.

module TopDown_term : sig ... end

Terminating top-down solver (topdown_term). Simpler version of Td3 without space-efficiency and incremental.

module TopDown_space_cache_term : sig ... end

Terminating top-down solver, which supports space-efficiency and caching (topdown_space_cache_term). Simpler version of Td3 without incremental.

module TopDown_deprecated : sig ... end

Deprecated top-down solver (topdown_deprecated).

SLR

The SLR solver family.

module SLRphased : sig ... end

Two-phased terminating SLR3 solver (slr3tp).

module SLRterm : sig ... end

Terminating SLR3 solver (slr3t). Simpler version of SLRphased without phases.

module SLR : sig ... end

Various SLR solvers.

Other

module EffectWConEq : sig ... end

(effectWConEq).

module Worklist : sig ... end

Worklist solver (WL).

module Generic : sig ... end

Various simple/old solvers and solver utilities.

module Selector : sig ... end

Solver, which delegates at runtime to the configured solver.

module PostSolver : sig ... end

Extra constraint system evaluation pass for warning generation, verification, pruning, etc.

module LocalFixpoint : sig ... end

Fixpoint iteration solvers local to a single transfer function (don't use a constraint system).

module SolverStats : sig ... end

Statistics for solvers.

module SolverBox : sig ... end

Box operator for warrowing solvers.

I/O

Various input/output interfaces and formats.

module Messages = Messages
module Tracing = Tracing

Front-end

The following modules handle program input.

module Preprocessor : sig ... end

Detection of suitable C preprocessor.

module CompilationDatabase : sig ... end

Input program from a real-world project using a compilation database.

module MakefileUtil : sig ... end

Input program from a real-world project using a Makefile.

module TerminationPreprocessing : sig ... end

Witnesses

Witnesses are an exchangeable format for analysis results.

module Svcomp : sig ... end

SV-COMP tasks and results.

module SvcompSpec : sig ... end

SV-COMP specification strings and files.

module Invariant : sig ... end

Invariants for witnesses.

module InvariantCil : sig ... end

Invariant manipulation related to CIL transformations.

module WitnessUtil : sig ... end

Utilities for witness generation and witness invariants.

GraphML

Automaton-based GraphML witnesses used in SV-COMP.

module MyARG : sig ... end

Abstract reachability graph.

module WitnessConstraints : sig ... end

Analysis specification transformation for ARG construction.

module ArgTools : sig ... end

Construction of ARGs from constraint system solutions.

module Witness : sig ... end

Output of ARG as GraphML.

module Graphml : sig ... end

Streaming GraphML output.

YAML

Entry-based YAML witnesses to be used in SV-COMP.

module YamlWitness : sig ... end

YAML witness generation and validation.

module YamlWitnessType : sig ... end

YAML witness format types.

module WideningTokens : sig ... end

Widening tokens are a generic and dynamic mechanism for delaying widening.

Violation

Experimental generation of violation witness automata or refinement with observer automata.

module Violation : sig ... end

Violation checking in an ARG.

Sourcemodule ViolationZ3 : sig ... end

ARG path feasibility checking using weakest precondition and Z3 (not installed!).

module ObserverAutomaton : sig ... end

Finite automaton for matching an infeasible ARG path.

module ObserverAnalysis : sig ... end

Path-sensitive analysis using an ObserverAutomaton.

module Refinement : sig ... end

Experimental analysis refinement.

SARIF

module Sarif : sig ... end

SARIF output of Messages.

module SarifType : sig ... end

SARIF format types.

module SarifRules : sig ... end

SARIF rule definitions for Goblint.

Transformations

Transformations can be activated to transform the program using analysis results.

module Transform : sig ... end

Signatures and registry for transformations.

module DeadCode : sig ... end

Dead code elimination transformation (remove_dead_code).

module EvalAssert : sig ... end

Transformation for instrumenting the program with computed invariants as assertions (assert).

module ExpressionEvaluation : sig ... end

Transformation for evaluating expressions on the analysis results (expeval). Hack for Gobview.

Utilities

module Timing = Timing
module GoblintDir : sig ... end

Intermediate data directory.

General

module IntOps : sig ... end

Unified interface for integer types.

module FloatOps : sig ... end

Unified interface for floating-point types.

module LazyEval = LazyEval
module ResettableLazy = ResettableLazy
module ProcessPool : sig ... end

Process pool for running processes in parallel.

module Timeout : sig ... end

Timeout utilities.

module TimeUtil : sig ... end

Date and time utilities.

module MessageUtil = MessageUtil
module XmlUtil = XmlUtil

CIL

module CilType = CilType
module Cilfacade = Cilfacade
module RichVarinfo = RichVarinfo
module CilCfg : sig ... end

Creation of CIL CFGs.

module LoopUnrolling : sig ... end

Syntactic loop unrolling.

Library specification

For more precise analysis of C standard library, etc functions, whose definitions are not available, custom specifications can be added.

module AccessKind : sig ... end

Kinds of memory accesses.

module LibraryDesc : sig ... end

Library function descriptor (specification).

module LibraryDsl : sig ... end

Library function descriptor DSL.

module LibraryFunctions : sig ... end

Hard-coded database of library function specifications.

Analysis-specific

module BaseUtil : sig ... end

Basic analysis utilities.

module PrecisionUtil : sig ... end

Integer and floating-point option and attribute handling.

module ContextUtil : sig ... end

Goblint-specific C attribute handling.

module BaseInvariant : sig ... end

Analyses.Spec.branch refinement for Base analysis.

module CommonPriv : sig ... end

Thread-modular value analysis utilities for BasePriv and RelationPriv.

module WideningThresholds : sig ... end

Widening threshold utilities.

module VectorMatrix : sig ... end

OCaml implementations of vectors and matrices.

Sourcemodule SharedFunctions : sig ... end

Precision comparison

module PrecCompare : sig ... end

Precison comparison.

module PrecCompareUtil : sig ... end

Signatures for precision comparison.

module PrivPrecCompareUtil : sig ... end

BasePriv precison comparison.

Sourcemodule RelationPrecCompareUtil : sig ... end
Sourcemodule ApronPrecCompareUtil : sig ... end

Library extensions

OCaml library extensions which are completely independent of Goblint.

See Goblint_std.

Standard library

OCaml standard library extensions which are not provided by Batteries.

module GobFormat = GobFormat

Other libraries

External library extensions.

module MyCheck = MyCheck