package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.

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

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct