package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

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

Authors

Maintainers

Sources

goblint-2.4.0.tbz

sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6

sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af

doc/goblint.lib/Goblint_lib/index.html

Module `Goblint_lib`Source

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 = 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.

Sourcemodule ConstrSys = ConstrSys

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.

Sourcemodule VarQuery = VarQuery

Configuration

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

Sourcemodule GobConfig = GobConfig

Sourcemodule AfterConfig = AfterConfig

Sourcemodule AutoTune : sig ... end

Autotuning of the configuration based on syntactic heuristics.

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.

Sourcemodule JsonSchema = JsonSchema

Sourcemodule 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

Sourcemodule LinearTwoVarEqualityAnalysis : 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 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

Sourcemodule Lattice = Lattice

General

Standard general-purpose domains and domain functors.

Sourcemodule BoolDomain = BoolDomain

Sourcemodule SetDomain = SetDomain

Sourcemodule MapDomain = MapDomain

Sourcemodule TrieDomain = TrieDomain

Sourcemodule DisjointDomain = DisjointDomain

Sourcemodule HoareDomain = HoareDomain

Sourcemodule PartitionDomain = PartitionDomain

Sourcemodule FlagHelper = FlagHelper

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.

Sourcemodule RelationDomain : sig ... end

Sourcemodule ApronDomain : sig ... end

Sourcemodule AffineEqualityDomain : sig ... end

Sourcemodule LinearTwoVarEqualityDomain : sig ... end

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.

Sourcemodule CompareCIL = CompareCIL

Sourcemodule CompareAST = CompareAST

Sourcemodule CompareCFG = CompareCFG

Sourcemodule UpdateCil = UpdateCil

Sourcemodule MaxIdUtil = MaxIdUtil

Sourcemodule Serialize = Serialize

Sourcemodule CilMaps = CilMaps

I/O

Various input/output interfaces and formats.

module Messages = Messages

Sourcemodule Logs = Goblint_logs.Logs

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.

Sourcemodule MakefileUtil = MakefileUtil

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 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 = 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

Sourcemodule AnsiColors = Goblint_logs.AnsiColors

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.

Sourcemodule AccessKind = AccessKind

Sourcemodule LibraryDesc = LibraryDesc

Sourcemodule LibraryDsl = LibraryDsl

Sourcemodule LibraryFunctions = LibraryFunctions

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.

Sourcemodule SharedFunctions : sig ... end

Sourcemodule GobApron : sig ... end

Precision comparison

module PrecCompare : sig ... end

Precision comparison.

module PrecCompareUtil : sig ... end

Signatures for precision comparison.

module PrivPrecCompareUtil : sig ... end

BasePriv precision 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

On This Page

Framework
Analyses
1. Value
2. Heap
3. Concurrency
  1. Locks
  2. Threads
  3. Other
4. Longjmp
5. Tutorial
6. Other
7. Helper
Domains
1. General
2. Analysis-specific
  1. Value
  2. Concurrency
  3. Other
3. Testing
Incremental
I/O
1. Front-end
2. Witnesses
  1. GraphML
  2. YAML
  3. Violation
3. SARIF
Transformations
Utilities
Library extensions
1. Standard library

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/index.html

Module Goblint_libSource

Framework

CFG

Specification

Results

Configuration

Analyses

Value

Heap

Concurrency

Locks

Threads

Other

Longjmp

Tutorial

Other

Helper

Domains

General

Analysis-specific

Value

Non-relational

Numeric

Addresses

Complex

Combined

Relational

Concurrency

Other

Testing

Incremental

I/O

Front-end

Witnesses

GraphML

YAML

Violation

SARIF

Transformations

Utilities

General

CIL

Library specification

Analysis-specific

Precision comparison

Library extensions

Standard library

Module `Goblint_lib`Source