package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
module AbstractionDomainProperties : sig ... end
module Access : sig ... end
module AccessAnalysis : sig ... end

Access and data race analysis.

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

Signatures for analyzers, analysis specifications, and result output.

module ApronAnalysis : sig ... end
module ApronDomain : sig ... end
module ApronPrecCompareUtil : sig ... end
module ApronPriv : sig ... end
module ArrayDomain : sig ... end
module Assert : 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 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.

module ConfigProfile : sig ... end
module 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 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 ExpDomain : 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 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 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

See LibraryFunctions implementation for example usage.

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

Basic lockset analyses.

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

Structures for the querying subsystem.

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 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 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
module Version : sig ... end
module Violation : sig ... end
module 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