package goblint

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Domains
1. General

goblint.backtrace
- Goblint_backtrace
goblint.build-info.dune
- Goblint_build_info
goblint.build-info.js
- Goblint_build_info
goblint.cdomain.value
- AddressDomain
  - AddressBase
    
    Mval
  - AddressLattice
    
    Mval
  - AddressLatticeRepr
    
    Mval
    
    UnitOffsetRepr
    
    VariableRepr
  - AddressPrintable
    
    Mval
  - AddressSet
    
    Addr
    
    ID
    
    Mval
- AddressDomain_intf
  - AddressDomain
    
    AddressBase
    
    Mval
    
    AddressLattice
    
    Mval
    
    AddressLatticeRepr
    
    Mval
    
    UnitOffsetRepr
    
    VariableRepr
    
    AddressPrintable
    
    Mval
    
    AddressSet
    
    Addr
    
    ID
    
    Mval
- ArrayDomain
  - AttributeConfiguredAndNullByteArrayDomain
    
    Idx
    
    Val
  - AttributeConfiguredArrayDomain
    
    Idx
    
    Val
  - LatticeWithInvalidate
  - LatticeWithNull
  - LatticeWithSmartOps
  - Null
  - NullByte
    
    Idx
    
    Val
  - Partitioned
    
    Idx
    
    Val
  - PartitionedWithLength
    
    Idx
    
    Val
  - S
  - S0
  - Str
  - StrWithDomain
  - Trivial
    
    Idx
    
    Val
  - TrivialWithLength
    
    Idx
    
    Val
- ConcDomain
- FloatDomain
- IntDomain
  - Arith
  - ArithIkind
  - B
  - BISet
  - Booleans
  - BooleansNames
  - Congruence
  - DefExc
  - Enums
  - Flat
    
    Base
  - FlatPureIntegers
  - Flattened
  - Ikind
  - IkindUnawareS
  - IntDomLifter
    
    I
  - IntDomTuple
  - IntDomWithDefaultIkind
    
    I
    
    Ik
  - Integers
    
    Ints_t
  - Interval
  - Interval32
  - IntervalFunctor
    
    Ints_t
  - IntervalSet
  - IntervalSetFunctor
    
    Ints_t
  - Lift
    
    Base
  - Lifted
  - MakeBooleans
    
    Names
  - PtrDiffIkind
  - Reverse
    
    Base
  - S
  - SOverflow
  - SOverflowUnlifter
    
    D
  - Size
  - Y
  - Z
- Invariant
  - ExpLat
  - N
- InvariantCil
- JmpBufDomain
- Lval
  - Set
- MutexAttrDomain
  - MutexKind
- Mval
  - Exp
  - MakeLattice
    
    Offs
  - MakePrintable
    
    Offs
  - Unit
  - Z
- Mval_intf
  - Lattice
  - Mval
    
    Exp
    
    MakeLattice
    
    Offs
    
    MakePrintable
    
    Offs
    
    Unit
    
    Z
  - Printable
- NullByteSet
  - MaySet
    
    M
  - MustMaySet
    
    Set
  - MustSet
    
    M
- Offset
  - Exp
  - Index
    
    Exp
    
    Printable
    
    Unit
    
    Z
  - MakeLattice
    
    Idx
  - MakePrintable
    
    Idx
  - Poly
  - Unit
  - Z
- Offset_intf
  - Index
    
    Printable
  - Lattice
  - Offset
    
    Exp
    
    Index
    
    Exp
    
    Printable
    
    Unit
    
    Z
    
    MakeLattice
    
    Idx
    
    MakePrintable
    
    Idx
    
    Poly
    
    Unit
    
    Z
  - Printable
- PreValueDomain
  - AD
    
    Addr
  - Addr
  - IndexDomain
  - Mval
  - Offs
- PrecisionUtil
- StringDomain
- StructDomain
  - Arg
  - FlagConfiguredStructDomain
    
    Val
  - KeyedSets
    
    Val
  - S
  - Sets
    
    Val
  - Simple
    
    Val
- ThreadIdDomain
  - FlagConfiguredTID
    
    D
  - FunNode
  - History
    
    Base
    
    D
  - Lift
    
    Thread
  - S
  - Stateful
    
    D
  - Stateless
  - Thread
    
    D
  - ThreadLiftNames
  - ThreadLifted
  - Unit
    
    Base
    
    D
- UnionDomain
  - Arg
  - Field
  - S
  - Simple
    
    Values
- ValueDomain
  - AddrSetDomain
  - Blob
    
    Size
    
    Value
  - Blobs
  - CArrays
  - Compound
  - InvariantArg
  - Offs
  - S
  - Structs
  - Unions
  - ValueInvariant
    
    Arg
    
    VS
  - ZeroInit
- ValueDomainQueries
  - ID
  - LS
- WideningThresholds
- WrapperFunctionAnalysis0
goblint.common
- AnalysisState
- AnalysisStateUtil
- Basetype
  - CilExp
  - CilStmt
  - RawBools
  - RawStrings
  - Variables
- CfgTools
  - CfgPrinters
    
    NodeStyles
  - NodeStyles
  - SCC
- CilCfg0
  - allBBVisitor
- CilLocation
- CilType
  - Attribute
  - Attributes
  - Attrparam
  - Binop
  - Compinfo
  - Constant
  - Encoding
  - Enuminfo
  - Exp
  - Fieldinfo
  - Fkind
  - Fundec
  - Ikind
  - Location
  - Lval
  - Offset
  - S
  - Std
  - Stmt
  - Typ
  - Typeinfo
  - Typsig
  - Unop
  - Varinfo
  - Wstring_type
- Cilfacade
  - FunLocH
  - IntH
  - LocSet
  - StmtH
  - StringH
  - VarinfoH
  - addConstructors
  - cleanCilPrinterClass
  - countFnVisitor
  - stmtSidVisitor
- Cilfacade0
- ContextUtil
- ControlSpecC
- Edge
- FloatOps
- GobFormat
- IntOps
  - BigIntOps
  - BigIntOpsBase
  - Int32Ops
  - Int32OpsBase
  - Int64Ops
  - Int64OpsBase
  - IntOps
  - IntOpsBase
  - IntOpsDecorator
    
    B
  - NIntOps
  - NIntOpsBase
- LazyEval
  - Make
    
    M
- LoopUnrolling0
  - CopyOfHashTable
- MessageCategory
  - Behavior
    
    Undefined
    
    ArrayOutOfBounds
  - Cast
  - Integer
- MessageUtil
- Messages
  - Location
  - Message
  - MultiPiece
  - Piece
  - Severity
  - Table
    
    MH
  - Tag
  - Tags
- MyCFG
  - CfgBackward
  - CfgBidir
  - CfgBidirSkip
  - CfgEdge
  - CfgEdgeH
    
    Exceptionless
    
    Infix
    
    Labels
  - CfgForward
  - FileCfg
    
    Cfg
  - NodeH
    
    Exceptionless
    
    Infix
    
    Labels
- Node
- Node0
- Printable
  - Chain
    
    P
  - ChainParams
  - DefaultConf
  - Either
    
    Base1
    
    Base2
  - Either3
    
    Base1
    
    Base2
    
    Base3
  - Either3Conf
    
    Base1
    
    Base2
    
    Base3
    
    Conf
  - EitherConf
    
    Base1
    
    Base2
    
    Conf
  - Empty
  - Failwith
    
    Message
  - FailwithMessage
  - Formatable
  - HConsed
    
    Base
    
    HC
  - HashCached
    
    LazyHash
    
    M
  - Lift2Conf
    
    Base1
    
    Base2
    
    Conf
  - LiftBot
    
    Base
  - LiftConf
    
    Base
    
    Conf
  - LiftTop
    
    Base
  - Liszt
    
    Base
  - Name
  - Option
    
    Base
    
    N
  - PQueue
    
    Base
  - PrefixName
    
    Base
    
    Conf
  - PrefixNameConf
  - Prettyable
  - Prod
    
    Base1
    
    Base2
  - Prod3
    
    Base1
    
    Base2
    
    Base3
  - Prod4
    
    Base1
    
    Base2
    
    Base3
    
    Base4
  - ProdConf
    
    Base1
    
    Base2
    
    C
  - ProdConfiguration
  - ProdSimple
    
    Base1
    
    Base2
  - S
  - Showable
  - SimpleFormat
    
    P
  - SimplePretty
    
    P
  - SimpleShow
    
    P
  - Std
  - StdLeaf
  - Strings
  - Unit
  - UnitConf
    
    N
  - Yojson
  - Z
- ResettableLazy
- RichVarinfo
  - BiVarinfoMap
    
    Collection
    
    Make
    
    X
    
    S
  - G
  - H
  - Make
    
    X
  - VarinfoMap
- Timing
  - Default
  - Program
- UpdateCil0
  - NodeMap
- XmlUtil
goblint.config
- AfterConfig
- GobConfig
  - Impl
  - S
  - Validator
  - ValidatorRequireAll
- JsonSchema
  - JE
  - JQ
  - JS
  - Schema
  - Validator
    
    Schema
- Options
goblint.constraint
- ConstrSys
  - CurrentVarEqConstrSys
    
    S
    
    Dom
    
    Var
  - EqConstrSys
    
    Dom
    
    Var
  - EqConstrSysFromGlobConstrSys
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
  - GenericEqIncrSolver
    
    Arg
    
    S
    
    Dom
    
    Var
  - GenericEqIncrSolverBase
    
    S
    
    Dom
    
    Var
  - GenericEqSolver
    
    S
    
    Dom
    
    Var
  - GenericGlobSolver
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
  - GlobConstrSolFromEqConstrSol
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    S2
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - GlobConstrSolFromEqConstrSolBase
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
  - GlobConstrSys
    
    D
    
    G
    
    GVar
    
    LVar
  - GlobSolverFromEqSolver
    
    EqSys
    
    Dom
    
    Var
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    Sol
    
    S
    
    Dom
    
    Var
    
    Sol'
    
    Splitter
  - IncrSolverArg
  - MonSystem
    
    Dom
    
    Var
  - SysVar
  - Var2
    
    GV
    
    LV
  - VarType
- VarQuery
goblint.domain
- BoolDomain
  - Bool
  - FlatBool
  - MayBool
  - MustBool
- DisjointDomain
  - CombinedSet
    
    B
    
    E
    
    RC
  - Congruence
  - MayEqualSetDomain
  - PairwiseMap
    
    B
    
    C
    
    E
    
    R
  - PairwiseSet
    
    B
    
    C
    
    E
  - ProjectiveMap
    
    B
    
    E
    
    R
    
    V
  - ProjectiveSet
    
    B
    
    E
    
    R
  - ProjectiveSetPairwiseMeet
    
    B
    
    E
    
    R
  - Representative
  - RepresentativeCongruence
- FlagHelper
  - FlagError
  - FlagHelper
    
    L
    
    Msg
    
    R
  - LatticeFlagHelper
    
    L
    
    Msg
    
    R
  - LatticeFlagHelperArg
- HoareDomain
  - HoarePO
    
    B
    
    E
  - MapBot
    
    R
    
    SpecD
  - Set
    
    B
  - SetEM
    
    E
  - SetS
  - Set_LiftTop
    
    B
    
    N
- Lattice
  - Chain
    
    P
  - Fake
    
    Base
  - FakeSingleton
    
    Base
  - Flat
    
    Base
  - FlatConf
    
    Base
    
    Conf
  - HConsed
    
    Arg
    
    Base
    
    HC
  - HashCached
    
    LazyHash
    
    M
  - Lift
    
    Base
  - Lift2
    
    Base1
    
    Base2
  - Lift2Conf
    
    Base1
    
    Base2
    
    Conf
  - LiftBot
    
    Base
  - LiftConf
    
    Base
    
    Conf
  - LiftPO
    
    Base
    
    Conf
  - LiftTop
    
    Base
  - Liszt
    
    Base
  - NoBotTop
  - Num
  - PD
  - PO
  - Prod
    
    Base1
    
    Base2
  - Prod3
    
    Base1
    
    Base2
    
    Base3
  - Prod4
    
    Base1
    
    Base2
    
    Base3
    
    Base4
  - ProdConf
    
    Base1
    
    Base2
    
    C
  - ProdList
    
    Base
    
    N
  - ProdSimple
    
    Base1
    
    Base2
  - Reverse
    
    Base
  - S
  - Unit
  - UnitConf
    
    N
- MapDomain
  - Bindings
  - Groupable
  - HConsed
    
    M
  - HashCached
    
    M
  - Joined
    
    E
    
    R
  - LiftBot
    
    M
    
    Range
  - LiftTop
    
    M
    
    Range
  - MapBot
    
    Domain
    
    Range
  - MapBot_LiftTop
    
    Domain
    
    Range
  - MapTop
    
    Domain
    
    Range
  - MapTop_LiftBot
    
    Domain
    
    Range
  - PMap
    
    Domain
    
    Range
  - PS
  - Print
    
    D
    
    M
    
    R
  - PrintGroupable
    
    D
    
    Group
    
    GroupMap
    
    M
    
    R
  - S
  - Timed
    
    M
- PartitionDomain
  - Collapse
  - CollapseSet
  - ExpPartitions
    
    B
    
    E
  - Make
    
    S
  - Set
    
    S
  - SetSet
    
    B
    
    Base
    
    E
- SetDomain
  - Elements
  - FiniteSet
    
    E
  - FiniteSetElem
  - HeadlessSet
    
    Base
  - Joined
    
    E
  - LiftTop
    
    N
    
    S
  - Make
    
    Base
  - Print
    
    E
    
    S
  - Reverse
    
    Base
  - S
  - SensitiveConf
    
    Base
    
    C
    
    Elt
    
    User
  - ToppedSet
    
    Base
    
    N
  - ToppedSetNames
- TrieDomain
  - Make
    
    ChildMap
    
    Key
    
    Trie
    
    Value
goblint.incremental
- CilMaps
- CompareAST
  - StringMap
- CompareCFG
  - NH
- CompareCIL
- MakefileUtil
- MaxIdUtil
- Serialize
  - Cache
- UpdateCil
goblint.lib
- Goblint_lib
  - AbortUnless
    
    Spec
  - AbstractionDomainProperties
    
    AbstractFunction
    
    AbstractTest
    
    AD
    
    CD
    
    Monotone
    
    AD
    
    AF
    
    CD
    
    ValidTest
    
    AD
    
    AF
    
    CD
  - Access
    
    A
    
    AS
    
    Memo
    
    MemoRoot
    
    TSH
    
    Exceptionless
    
    Infix
    
    Labels
    
    WarnAccs
  - AccessAnalysis
    
    Spec
    
    C
    
    V
  - AccessDomain
    
    Event
    
    EventSet
  - ActiveLongjmp
    
    Spec
  - ActiveSetjmp
    
    Spec
    
    C
    
    P
  - AffineEqualityAnalysis
  - AffineEqualityDomain
  - Analyses
    
    DefaultSpec
    
    Dom
    
    LD
    
    EmptyV
    
    GVarF
    
    V
    
    GVarFC
    
    C
    
    V
    
    GVarG
    
    C
    
    CSet
    
    G
    
    IdentityP
    
    D
    
    IdentitySpec
    
    IdentityUnitContextsSpec
    
    MCPA
    
    MCPSpec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    SpecSysSol
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    SpecSysVar
    
    StdV
    
    UnitA
    
    UnitP
    
    UnitV
    
    ValueContexts
    
    D
    
    Var
    
    VarF
    
    LD
    
    VarinfoV
  - AnalysisResult
    
    Result
    
    C
    
    Exceptionless
    
    Infix
    
    Labels
    
    Range
    
    ResultConf
    
    ResultNode
    
    ResultType2
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
  - ApronAnalysis
  - ApronDomain
  - ApronPrecCompareUtil
  - ArgTools
    
    BiArg
    
    Node
    
    Dot
    
    Arg
    
    Node
    
    NodeStyles
    
    Make
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Node
    
    Query
    
    R
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    NodeStyles
  - Assert
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - AutoSoundConfig
  - AutoTune
    
    FunctionCallMap
    
    FunctionSet
    
    VariableMap
    
    VariableSet
    
    addTypeAttributeVisitor
    
    collectFunctionCallsVisitor
    
    enumVisitor
    
    functionVisitor
    
    modFunctionAnnotatorVisitor
    
    modVisitor
    
    octagonFunctionVisitor
    
    octagonVariableVisitor
  - Base
    
    MainFunctor
    
    C
    
    Dom
    
    G
    
    Invariant
    
    InvariantEval
    
    Priv
    
    D
    
    G
    
    V
    
    RVEval
    
    V
    
    VarH
    
    Exceptionless
    
    Infix
    
    Labels
    
    VarMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    MainSpec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - BaseDomain
    
    BaseComponents
    
    PrivD
    
    CPA
    
    M
    
    Group
    
    GroupMap
    
    M0
    
    DomFunctor
    
    ExpEval
    
    PrivD
    
    DomWithTrivialExpEval
    
    PrivD
    
    ExpEvaluator
    
    PartDeps
    
    VarSet
    
    WeakUpdates
  - BaseInvariant
    
    Eval
    
    D
    
    G
    
    V
    
    Make
    
    Eval
    
    D
    
    G
    
    V
  - BasePriv
    
    S
    
    D
    
    G
    
    V
  - BaseUtil
  - Callstring
    
    Callsite
    
    Callstring
    
    CallstringType
    
    Spec
    
    A
    
    C
    
    CT
    
    D
    
    G
    
    P
    
    V
  - CilCfg
    
    allBBVisitor
    
    countLoopsVisitor
  - CommonPriv
    
    AtomicParam
    
    ConfCheck
    
    RequireMutexActivatedInit
    
    RequireMutexPathSensOneMainInit
    
    RequireThreadFlagPathSensInit
    
    Digest
    
    Locksets
    
    MinLocksets
    
    MayVars
    
    MustVars
    
    MutexGlobals
    
    V
    
    VGlobal
    
    VMutex
    
    VMutexInits
    
    NoAtomic
    
    PerMutexTidCommon
    
    D
    
    Digest
    
    G
    
    GMutex
    
    GThread
    
    L
    
    LD
    
    LLock
    
    LMust
    
    V
    
    W
    
    Protection
    
    ThreadDigest
    
    ThreadNotStartedDigest
    
    WriteCenteredD
    
    P
    
    W
  - CompilationDatabase
  - CondVars
    
    Domain
    
    Spec
    
    C
  - Constants
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - Constraints
    
    CompareEqSys
    
    Compare
    
    CompareD
    
    Var
    
    Sys
    
    Dom
    
    Var
    
    CompareGlobSys
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    CompareGlobal
    
    Compare
    
    CompareD
    
    Var
    
    G
    
    GVar
    
    CompareHashtbl
    
    CompareD
    
    Dom
    
    Var
    
    CompareNode
    
    C
    
    Compare
    
    CompareD
    
    Var
    
    D
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Node
    
    ContextGasLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    DeadBranchLifter
    
    C
    
    D
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    DeadCodeLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    FromSpec
    
    Cfg
    
    I
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    HashconsContextLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    HashconsLifter
    
    D
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    Increment
    
    IntConf
    
    LevelSliceLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    LimitLifter
    
    C
    
    D
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    LongjmpLifter
    
    C
    
    D
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    NoContext
    
    OptEqual
    
    C
    
    D
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    PathSensitive2
    
    D
    
    P
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    RecursionTermLifter
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    WidenContextLifterSide
    
    D
    
    DD
    
    M
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
  - Control
    
    AnalyzeCFG
    
    Cfg
    
    CompareGlobSys
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    Sys
    
    D
    
    G
    
    CSet
    
    GVar
    
    LVar
    
    Inc
    
    LT
    
    PostSolverArg
    
    Query
    
    RT
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    Slvr
    
    EqSys
    
    Dom
    
    Var
    
    Sol'
    
    Splitter
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    SpecSys
    
    EQSys
    
    S2S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    X
    
    C
    
    D
    
    G
    
    P
    
    V
  - DeadCode
    
    RemoveDeadCode
  - Deadlock
    
    Spec
    
    A
    
    Arg
    
    G
    
    V
    
    C
    
    D
    
    LockEventPair
    
    MayLockEventPairs
    
    P
    
    V
  - DeadlockDomain
    
    LockEvent
    
    MayLockEvents
  - DomainProperties
    
    All
    
    D
    
    AllNonAssoc
    
    D
    
    Bot
    
    D
    
    Connect
    
    D
    
    DomainTest
    
    D
    
    Equal
    
    D
    
    Join
    
    D
    
    Leq
    
    D
    
    Meet
    
    D
    
    Narrow
    
    D
    
    S
    
    Top
    
    D
    
    Widen
    
    D
  - EscapeDomain
    
    EscapedVars
  - EvalAssert
    
    EvalAssert
    
    visitor
  - Events
  - ExpRelation
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - ExpressionEvaluation
    
    ExpEval
  - Expsplit
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - ExtractPthread
    
    Action
    
    Codegen
    
    Action
    
    AdjacencyMatrix
    
    HashtblN
    
    Exceptionless
    
    Infix
    
    Labels
    
    PmlResTbl
    
    FunTbl
    
    Writer
    
    Edges
    
    Env
    
    Resource
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    Tasks
    
    Tbls
    
    CondVarIdTbl
    
    CtxTbl
    
    FunCallTbl
    
    FunNameToTids
    
    MutexMidTbl
    
    NodeTbl
    
    SymTbl
    
    G
    
    SymTblGen
    
    Tbl
    
    G
    
    TblGen
    
    ThreadTidTbl
    
    Variable
    
    Variables
    
    uniqueVarPrinterClass
  - GobApron
  - GobExn
  - GoblintDir
  - Graphml
    
    ArgNodeGraphMlWriter
    
    M
    
    N
    
    DeDupGraphMlWriter
    
    M
    
    EnumerateNodeGraphMlWriter
    
    M
    
    GraphMlWriter
    
    StringGraphMlWriter
    
    XmlGraphMlWriter
  - IntDomainProperties
    
    All
    
    D
    
    Ikind
    
    AllNonAssoc
    
    D
    
    Ikind
    
    IntegerSet
    
    Base
    
    Ikind
    
    OldS
    
    OldSWithIkind
    
    Ikind
    
    S
    
    Valid
    
    AD
    
    Ikind
    
    AF
    
    CD
    
    Base
    
    WithIkind
    
    I
    
    Ik
    
    Ikind
  - LinearTwoVarEqualityAnalysis
  - LinearTwoVarEqualityDomain
  - LockDomain
    
    AddrRW
    
    MakeRW
    
    P
    
    MayLocksetNoRW
    
    MustLock
    
    MustLockRW
    
    MustLockset
    
    MustLocksetRW
    
    MustMultiplicity
    
    Count
    
    MvalRW
  - LocksetAnalysis
    
    DS
    
    Make
    
    C
    
    D
    
    MakeMay
    
    A
    
    Arg
    
    D
    
    G
    
    V
    
    C
    
    D
    
    P
    
    MakeMust
    
    A
    
    Arg
    
    D
    
    G
    
    V
    
    C
    
    D
    
    P
    
    MayArg
    
    D
    
    G
    
    V
    
    MustArg
    
    D
    
    G
    
    V
  - LoopTermination
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    Statements
  - LoopUnrolling
  - LoopfreeCallstring
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - MCP
    
    MCP2
  - MCPAccess
    
    A
  - MCPRegistry
    
    AccListSpec
    
    ContextListSpec
    
    DomListLattice
    
    DLSpec
    
    DomListPrintable
    
    DLSpec
    
    DomListRepresentative
    
    DLSpec
    
    DomVariantLattice
    
    DLSpec
    
    DomVariantLattice0
    
    DLSpec
    
    DomVariantPrintable
    
    DLSpec
    
    DomVariantSysVar
    
    DLSpec
    
    DomainListLatticeSpec
    
    DomainListMCPASpec
    
    DomainListPrintableSpec
    
    DomainListRepresentativeSpec
    
    DomainListSysVarSpec
    
    GlobalDomainListSpec
    
    LocalDomainListSpec
    
    PathListSpec
    
    PrintableOfLatticeSpec
    
    D
    
    PrintableOfMCPASpec
    
    D
    
    PrintableOfRepresentativeSpec
    
    D
    
    PrintableOfSysVarSpec
    
    D
    
    VarListSpec
  - MHP
  - MHPAnalysis
    
    Spec
    
    A
  - Maingoblint
  - MallocFresh
    
    Spec
    
    A
    
    C
    
    D
  - Malloc_null
    
    Spec
    
    C
    
    P
  - MayLocks
    
    Arg
    
    D
    
    G
    
    V
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - MemLeak
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    ToppedVarInfoSet
  - MemOutOfBounds
    
    Spec
    
    C
  - ModifiedSinceSetjmp
    
    Spec
  - MusteqDomain
    
    Equ
    
    F
    
    P
    
    VF
  - MutexAnalysis
    
    Spec
    
    A
    
    Arg
    
    D
    
    G
    
    GProtected
    
    GProtecting
    
    MakeP
    
    G0
    
    P
    
    ReadWrite
    
    Write
    
    V
    
    C
    
    GM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    VarSet
  - MutexEventsAnalysis
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - MutexTypeAnalysis
    
    Spec
    
    A
    
    G
    
    P
    
    V
  - MyARG
    
    CFGEdge
    
    CfgIntra
    
    Cfg
    
    Edge
    
    InlineEdge
    
    InlineEdgePrintable
    
    InterestingArg
    
    Arg
    
    Edge
    
    Node
    
    IsInteresting
    
    Intra
    
    Arg
    
    Edge
    
    Node
    
    ArgIntra
    
    IsInteresting
    
    Node
    
    S
    
    Edge
    
    Node
    
    SIntra
    
    SIntraOpt
    
    Stack
    
    Arg
    
    Node
    
    StackNode
    
    Node
    
    UnCilLogicIntra
    
    Arg
    
    UnCilTernaryIntra
    
    Arg
  - ObserverAnalysis
    
    MakePathSpec
    
    A
    
    Arg
    
    C
    
    D
    
    G
    
    P
    
    V
    
    MakeSpec
    
    A
    
    Automaton
    
    C
    
    D
    
    G
    
    P
    
    V
    
    PathArg
    
    StepObserverAutomaton
  - ObserverAutomaton
    
    KMP
    
    KMPArg
    
    KMPArg
    
    S
  - PoisonVariables
    
    Spec
    
    VS
  - PrecCompare
    
    Comparison
    
    Make
    
    D
    
    MakeDump
    
    CompareDump
    
    CompareD
    
    Util
    
    Dom
    
    Key
    
    MakeHashtbl
    
    CompareD
    
    D
    
    K
  - PrecCompareUtil
    
    LocalizedPrintable
    
    R
    
    Dom
    
    Key
    
    S
    
    Dom
    
    Key
    
    Util
    
    Dom
    
    Key
  - Preprocessor
    
    FpathH
    
    Exceptionless
    
    Infix
    
    Labels
  - PrivPrecCompareUtil
    
    LV
    
    Util
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
  - ProcessPool
  - PthreadDomain
    
    D
    
    Pred
  - PthreadSignals
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - PtranalAnalysis
    
    Spec
  - Queries
    
    Any
    
    ES
    
    FlatYojson
    
    Hashtbl
    
    Exceptionless
    
    Infix
    
    Labels
    
    Protection
    
    Result
    
    SD
    
    Set
    
    Exceptionless
    
    Labels
    
    TS
    
    ThreadNodeLattice
    
    VI
    
    VS
  - RaceAnalysis
    
    Spec
    
    G
    
    MemoSet
    
    OffsetTrie
    
    ChildMap
    
    Trie
    
    OneOffset
    
    V
  - Refinement
  - Region
    
    Spec
    
    A
    
    C
    
    Lvals
    
    V
  - RegionDomain
    
    B
    
    RS
    
    Reg
    
    RegMap
    
    RegPart
    
    S
    
    RegionDom
    
    VFB
  - RelationAnalysis
  - RelationDomain
  - RelationPrecCompareUtil
  - RelationPriv
  - ResultQuery
    
    Make
    
    FileCfg
    
    Cfg
    
    SpecSysSol
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Query
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    SpecSysSol2
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
  - ReturnUtil
  - Sarif
  - SarifRules
  - SarifType
    
    Artifact
    
    ArtifactLocation
    
    Invocation
    
    Location
    
    Message
    
    PhysicalLocation
    
    Region
    
    ReportingDescriptor
    
    Result
    
    Run
    
    SarifLog
    
    Tool
    
    ToolComponent
  - Server
    
    ArgWrapper
    
    Arg
    
    Node
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Function
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ParamParser
    
    R
    
    Registry
    
    Request
  - SharedFunctions
  - Signs
    
    SL
    
    Signs
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - StackDomain
    
    Dom1
    
    Var
    
    VarLat
    
    Dom2
    
    Dom3
    
    Loc
    
    S
  - StackTrace
    
    Spec
    
    C
    
    D
    
    N
    
    Spec1
    
    A
    
    C
    
    D
    
    P
    
    V
    
    Spec2
    
    A
    
    C
    
    D
    
    P
    
    V
    
    SpecLoc
    
    C
  - Svcomp
    
    Result
    
    StackTaskResult
    
    Arg
    
    Edge
    
    Node
    
    TaskResult
    
    Arg
    
    Node
    
    Task
    
    Cfg
    
    TaskResult
    
    Arg
    
    Edge
    
    Node
  - SvcompSpec
  - SymbLocks
    
    PS
    
    Spec
    
    A
    
    E
    
    PLock
    
    C
  - SymbLocksDomain
    
    Exp
    
    ILock
    
    Idx
    
    LockingPattern
    
    Symbolic
    
    S
  - Taint
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    VarinfoSet
  - TaintPartialContexts
    
    Spec
    
    VS
  - TerminationPreprocessing
    
    VarToStmt
    
    loopCounterVisitor
  - ThreadAnalysis
    
    Spec
    
    C
    
    P
    
    V
  - ThreadEscape
    
    Spec
    
    C
    
    ThreadIdSet
  - ThreadFlag
    
    Spec
    
    A
    
    C
    
    P
  - ThreadFlagDomain
    
    S
    
    Simple
    
    Trivial
  - ThreadId
    
    Spec
    
    A
    
    C
    
    Created
    
    Callees
    
    Current
    
    D
    
    N
    
    P
    
    VNI
  - ThreadJoins
    
    Spec
    
    C
    
    D
    
    V
  - ThreadReturn
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - TimeUtil
  - Timeout
    
    Js
    
    Unix
  - TmpSpecial
    
    Spec
    
    D
    
    Deps
    
    MLDeps
  - Transform
    
    PartialEval
    
    visitor
    
    S
  - UnassumeAnalysis
    
    EH
    
    FH
    
    Spec
    
    D
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
  - Uninit
    
    Spec
    
    C
    
    P
  - UnitAnalysis
    
    Spec
  - UseAfterFree
    
    AllocaVars
    
    HeapVars
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    StackAndHeapVars
    
    ThreadIdToJoinedThreadsMap
  - VarEq
    
    Spec
    
    C
    
    D
  - VectorMatrix
    
    AbstractMatrix
    
    A
    
    V
    
    A
    
    AbstractVector
    
    A
    
    ArrayMatrix
    
    A
    
    V
    
    A
    
    ArrayVector
    
    A
    
    ConvenienceOps
    
    A
    
    Matrix
    
    RatOps
    
    Vector
  - Violation
    
    Feasibility
    
    Node
    
    PathArg
    
    Node
    
    UnknownFeasibility
    
    Node
    
    ViolationArg
    
    Node
  - ViolationZ3
  - Vla
    
    Spec
  - WideningTokens
    
    Dom
    
    D
    
    Lifter
    
    C
    
    D
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    TS
  - Witness
    
    Result
    
    ArgTool
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Node
    
    Query
    
    BiArgInvariant
    
    Node
    
    Query
    
    R
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    WitnessTaskResult
    
    Arg
    
    Node
  - WitnessConstraints
    
    PathSensitive3
    
    C
    
    D
    
    G
    
    P
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
  - WitnessUtil
    
    Invariant
    
    FileCfg
    
    Cfg
    
    InvariantExp
    
    ES
    
    InvariantParser
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    NH
    
    NS
    
    YamlInvariant
    
    FileCfg
    
    Cfg
    
    YamlInvariantValidate
    
    FileCfg
    
    Cfg
  - WrapperFunctionAnalysis
    
    MallocWrapper
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    SpecBase
    
    C
    
    D
    
    NodeFlatLattice
    
    UniqueCallCounter
    
    UniqueCount
    
    WrapperArgs
    
    ThreadCreateWrapper
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    WrapperArgs
  - YamlWitness
    
    Entry
    
    Make
    
    FCMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    FMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    R
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    WitnessInvariant
    
    ValidationResult
    
    ChainParams
    
    Validator
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    R
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
    
    WitnessInvariant
  - YamlWitnessType
    
    Certification
    
    Entry
    
    EntryType
    
    FlowInsensitiveInvariant
    
    Invariant
    
    InvariantSet
    
    Invariant
    
    InvariantType
    
    LocationInvariant
    
    LoopInvariant
    
    Location
    
    LocationInvariant
    
    LoopInvariant
    
    LoopInvariantCertificate
    
    Metadata
    
    PreconditionLoopInvariant
    
    PreconditionLoopInvariantCertificate
    
    Producer
    
    Target
    
    Task
goblint.library
goblint.logs
- Goblint_logs
  - AnsiColors
  - Logs
    
    Batteries
    
    BatteriesKind
    
    Format
    
    FormatKind
    
    Kind
    
    Level
    
    MakeKind
    
    Kind
    
    Pretty
    
    PrettyKind
    
    Result
goblint.sites.dune
- Goblint_sites
goblint.sites.js
- Goblint_sites
goblint.solver
- Goblint_solver
  - EffectWConEq
    
    Make
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - Generic
    
    DirtyBoxSolver
    
    S
    
    Dom
    
    Var
    
    LoadRunIncrSolver
    
    Arg
    
    S
    
    Dom
    
    Var
    
    LoadRunSolver
    
    S
    
    Dom
    
    Var
    
    PreciseSideEffectBoxSolver
    
    S
    
    Dom
    
    Var
    
    SolverStats
    
    S
    
    Dom
    
    Var
    
    SoundBoxSolver
    
    S
    
    Dom
    
    Var
    
    SoundBoxSolverImpl
    
    S
    
    Dom
    
    Var
  - LocalFixpoint
    
    Make
    
    D
  - PostSolver
    
    Compose
    
    PS1
    
    S
    
    Dom
    
    Var
    
    PS2
    
    EqConstrSysFromStartEqConstrSys
    
    S
    
    Dom
    
    Var
    
    EqIncrSolverFromEqSolver
    
    Arg
    
    S
    
    Dom
    
    Var
    
    Sol
    
    S
    
    Dom
    
    Var
    
    F
    
    S
    
    Dom
    
    Var
    
    IncrS
    
    S
    
    Dom
    
    Var
    
    ListArgFromStdArg
    
    Arg
    
    M
    
    S
    
    Dom
    
    Var
    
    MakeIncr
    
    PS
    
    S
    
    Dom
    
    Var
    
    MakeIncrList
    
    Arg
    
    M
    
    S
    
    Dom
    
    Var
    
    MakeIncrListArg
    
    M
    
    S
    
    Dom
    
    Var
    
    MakeList
    
    Arg
    
    M
    
    S
    
    Dom
    
    Var
    
    IncrArg
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    MakeListArg
    
    M
    
    S
    
    Dom
    
    Var
    
    MakeStdArg
    
    Prune
    
    S
    
    Dom
    
    Var
    
    S
    
    S
    
    Dom
    
    Var
    
    SaveRun
    
    S
    
    Dom
    
    Var
    
    StartEqConstrSys
    
    Dom
    
    Var
    
    Unit
    
    S
    
    Dom
    
    Var
    
    Verify
    
    S
    
    Dom
    
    Var
    
    Warn
    
    S
    
    Dom
    
    Var
  - SLR
    
    JustWiden
    
    D
    
    H
    
    HeapCompare
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    Make
    
    D
    
    H
    
    HeapCompare
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    Make0
    
    Box
    
    D
    
    D
    
    H
    
    HeapCompare
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    MyGenericEqSolver
    
    S
    
    Dom
    
    Var
    
    X
    
    PrintInfluence
    
    S
    
    Dom
    
    Var
    
    S1
    
    X
    
    Sol
    
    S
    
    Dom
    
    Var
    
    X
    
    SLR3
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
    
    TwoPhased
    
    N
    
    D
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    V
    
    W
    
    D
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    Version
  - SLRphased
    
    Make
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - SLRterm
    
    SLR3term
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - Selector
    
    Make
    
    Arg
    
    S
    
    Dom
    
    Var
  - SolverBox
    
    NarrowOption
    
    D
    
    S
    
    D
    
    Warrow
    
    D
    
    Widen
    
    D
  - SolverStats
  - Td3
    
    Base
    
    Arg
    
    CurrentVarS
    
    S
    
    Dom
    
    Var
    
    Hooks
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
    
    Basic
    
    Arg
    
    S
    
    Dom
    
    Var
    
    DepVals
    
    Arg
    
    S
    
    Dom
    
    Var
    
    Hooks
    
    S
    
    Dom
    
    Var
  - TopDown
    
    WP
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - TopDown_deprecated
    
    TD3
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - TopDown_space_cache_term
    
    WP
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - TopDown_term
    
    WP
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - Worklist
    
    Make
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
goblint.std
- Goblint_std
  - GobArray
  - GobFpath
  - GobGc
  - GobHashtbl
  - GobList
    
    Syntax
  - GobOption
    
    Syntax
  - GobPretty
  - GobQCheck
    
    Arbitrary
    
    Gen
    
    Iter
    
    Shrink
  - GobRef
  - GobResult
    
    Syntax
  - GobSys
  - GobUnix
  - GobYaml
  - GobYojson
  - GobZ
goblint.timing
- Goblint_timing
  - Make
    
    Name
  - Name
  - S
goblint.tracing
- Goblint_tracing
  - Strs

Legend:
Library
Module
Module type
Parameter
Class
Class type

Library goblint.domain

This library is unwrapped and provides the following top-level modules. For better context, see Goblint_lib which also documents these modules.

Domains

Lattice Signature for lattices. Functors for common lattices.

General

BoolDomain Boolean domains.
SetDomain Set domains.
MapDomain Map domains.
TrieDomain Trie domains.
DisjointDomain Abstract domains for collections of elements from disjoint unions of domains. Formally, the elements form a cofibered domain from a discrete category.
HoareDomain Abstract domains with Hoare ordering.
PartitionDomain Partitioning domains.
FlagHelper Domain alternatives chosen by a runtime flag.