package goblint

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package goblint

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

EqConstrSys where current_var indicates the variable whose right-hand side is currently being evaluated.

Parameters

module S : EqConstrSys

Signature

val current_var : S.v option Stdlib.ref

module S : sig ... end