package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af
doc/goblint.lib/Goblint_lib/index.html
Module Goblint_lib
Source
Main library.
Framework
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 = CfgTools
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 = AnalysisStateUtil
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 AnalysisResult : sig ... end
Analysis result output.
module ResultQuery : sig ... end
Perform queries on the constraint system solution.
Configuration
Runtime configuration is represented as JSON. Options are specified and documented by the JSON schema src/config/options.schema.json
.
module AutoSoundConfig : sig ... end
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.
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
).
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 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 ModifiedSinceSetjmp : sig ... end
Analysis of variables modified since setjmp
(modifiedSinceSetjmp
).
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 LoopTermination : sig ... end
Termination analysis for loops and goto
statements (termination
).
module Callstring : sig ... end
Call String analysis call_string
and/or Call Site analysis call_site
. The call string limitation for both approaches can be adjusted with the "callString_length" option. By adding new implementations of the CallstringType, additional analyses can be added.
module LoopfreeCallstring : sig ... end
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
).
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
).
module PtranalAnalysis : sig ... end
CIL's GoblintCil.Ptranal
for function pointer evaluation (ptranal
).
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
General
Standard general-purpose domains and domain functors.
Analysis-specific
Domains for specific analyses.
Value
Non-relational
Domains for Base
analysis.
Numeric
module IntDomain = IntDomain
module FloatDomain = FloatDomain
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 = Mval
module Offset = Offset
module StringDomain = StringDomain
module AddressDomain = AddressDomain
Complex
module StructDomain = StructDomain
module UnionDomain = UnionDomain
module ArrayDomain = ArrayDomain
module NullByteSet = NullByteSet
module JmpBufDomain = JmpBufDomain
Combined
These combine the above domains together for Base
analysis.
module BaseDomain : sig ... end
Full domain of Base
analysis.
module ValueDomain = ValueDomain
module ValueDomainQueries = ValueDomainQueries
Relational
Domains for RelationAnalysis
.
Concurrency
module MutexAttrDomain = MutexAttrDomain
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 = ThreadIdDomain
module ConcDomain = ConcDomain
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 = 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 StackDomain : sig ... end
Call stack domains.
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.
I/O
Various input/output interfaces and formats.
module Messages = Messages
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 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 = Invariant
module InvariantCil = InvariantCil
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 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.
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 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 = IntOps
module FloatOps = FloatOps
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
module GobExn : sig ... end
Exception utilities.
CIL
module CilType = CilType
module Cilfacade = Cilfacade
module CilLocation = CilLocation
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.
Analysis-specific
module BaseUtil : sig ... end
Basic analysis utilities.
module PrecisionUtil = PrecisionUtil
module ContextUtil = ContextUtil
module ReturnUtil : sig ... end
Special variable for return value.
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 = WideningThresholds
module VectorMatrix : sig ... end
OCaml implementations of vectors and matrices.
Precision comparison
module PrecCompare : sig ... end
Precision comparison.
module PrecCompareUtil : sig ... end
Signatures for precision comparison.
module PrivPrecCompareUtil : sig ... end
BasePriv
precision comparison.
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