Module `Goblint_lib`Source

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.

Sourcemodule ApronAnalysis : sig ... end

Sourcemodule ApronDomain : sig ... end

Sourcemodule ApronPrecCompareUtil : sig ... end

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

Sourcemodule ConfigProfile : sig ... end

Sourcemodule 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

Sourcemodule 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

Sourcemodule 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

Sourcemodule Version : sig ... end

module Violation : sig ... end

Sourcemodule 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/index.html

Module `Goblint_lib`Source

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/index.html

Module Goblint_libSource

Module `Goblint_lib`Source