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.common
- AfterConfig
- AnalysisState
- Basetype
  - Bools
  - CilExp
  - CilStmt
  - RawBools
  - RawStrings
  - Strings
  - Variables
- 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
  - countFnVisitor
  - stmtSidVisitor
- Cilfacade0
- ControlSpecC
- Edge
- GobConfig
  - Impl
  - S
  - Validator
  - ValidatorRequireAll
- GobFormat
- JsonSchema
  - JE
  - JQ
  - JS
  - Schema
  - Validator
    
    Schema
- Lattice
  - Chain
    
    P
  - Fake
    
    Base
  - FakeSingleton
    
    Base
  - Flat
    
    Base
    
    N
  - HConsed
    
    Base
    
    HC
  - HashCached
    
    LazyHash
    
    M
  - Lift
    
    Base
    
    N
  - Lift2
    
    Base1
    
    Base2
    
    N
  - LiftBot
    
    Base
  - LiftPO
    
    Base
    
    N
  - 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
- LazyEval
  - Make
    
    M
- MessageCategory
  - Behavior
    
    Undefined
    
    ArrayOutOfBounds
  - Cast
  - Integer
- MessageUtil
- Messages
  - Location
  - Message
  - MultiPiece
  - Piece
  - Severity
  - Table
    
    MH
  - Tag
  - Tags
- MyCFG
  - CfgBackward
  - CfgBidir
  - CfgForward
  - FileCfg
    
    Cfg
  - NodeH
    
    Exceptionless
    
    Infix
    
    Labels
- MyCheck
  - Arbitrary
  - Gen
  - Iter
  - Shrink
- Node
- Node0
- Options
- Printable
  - Chain
    
    P
  - ChainParams
  - DefaultNames
  - Either
    
    Base1
    
    Base2
  - Empty
  - Failwith
    
    Message
  - FailwithMessage
  - HConsed
    
    Base
    
    HC
  - HashCached
    
    LazyHash
    
    M
  - Lift
    
    Base
    
    N
  - Lift2
    
    Base1
    
    Base2
    
    N
  - LiftBot
    
    Base
  - LiftTop
    
    Base
  - LiftingNames
  - Liszt
    
    Base
  - Name
  - Option
    
    Base
    
    N
  - Prettyable
  - Prod
    
    Base1
    
    Base2
  - Prod3
    
    Base1
    
    Base2
    
    Base3
  - Prod4
    
    Base1
    
    Base2
    
    Base3
    
    Base4
  - ProdConf
    
    Base1
    
    Base2
    
    C
  - ProdConfiguration
  - ProdSimple
    
    Base1
    
    Base2
  - S
  - Showable
  - SimplePretty
    
    P
  - SimpleShow
    
    P
  - Std
  - StdLeaf
  - Strings
  - Unit
  - UnitConf
    
    N
  - Yojson
- ResettableLazy
- RichVarinfo
  - BiVarinfoMap
    
    Collection
    
    Make
    
    X
    
    S
  - G
  - H
  - Make
    
    X
  - VarinfoMap
- Timing
  - Default
  - Program
- Tracing
  - Strs
- UpdateCil0
  - NodeMap
- XmlUtil
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
    
    V
  - AccessDomain
    
    Event
    
    EventSet
  - AccessKind
  - ActiveLongjmp
    
    Spec
  - ActiveSetjmp
    
    Spec
    
    P
  - AddressDomain
    
    AddressBase
    
    Mval
    
    AddressLattice
    
    Mval
    
    AddressLatticeRepr
    
    Mval
    
    UnitOffsetRepr
    
    VariableRepr
    
    AddressPrintable
    
    Mval
    
    AddressSet
    
    Addr
    
    ID
    
    Mval
  - AffineEqualityAnalysis
  - AffineEqualityDomain
  - Analyses
    
    DefaultSpec
    
    Dom
    
    LD
    
    EmptyV
    
    EqConstrSys
    
    Dom
    
    Var
    
    GVarF
    
    V
    
    GVarFC
    
    C
    
    V
    
    GVarG
    
    C
    
    CSet
    
    G
    
    GenericEqIncrSolver
    
    Arg
    
    S
    
    Dom
    
    Var
    
    GenericEqIncrSolverBase
    
    S
    
    Dom
    
    Var
    
    GenericEqSolver
    
    S
    
    Dom
    
    Var
    
    GenericGlobSolver
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    GlobConstrSys
    
    D
    
    G
    
    GVar
    
    LVar
    
    IdentityP
    
    D
    
    IdentitySpec
    
    IncrSolverArg
    
    MCPA
    
    MCPSpec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    MonSystem
    
    Dom
    
    Var
    
    Result
    
    C
    
    Exceptionless
    
    Infix
    
    Labels
    
    Range
    
    ResultConf
    
    ResultNode
    
    ResultType2
    
    S
    
    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
    
    SysVar
    
    UnitA
    
    UnitP
    
    UnitV
    
    Var
    
    VarF
    
    LD
    
    VarType
    
    VarinfoV
  - AnalysisStateUtil
  - ApronAnalysis
  - ApronDomain
  - ApronPrecCompareUtil
  - ArgTools
    
    BiArg
    
    Node
    
    Dot
    
    Arg
    
    Node
    
    Make
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Node
    
    Query
    
    R
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    P
    
    V
  - ArrayDomain
    
    AttributeConfiguredArrayDomain
    
    Idx
    
    Val
    
    LatticeWithSmartOps
    
    Partitioned
    
    Idx
    
    Val
    
    PartitionedWithLength
    
    Idx
    
    Val
    
    S
    
    Trivial
    
    Idx
    
    Val
    
    TrivialWithLength
    
    Idx
    
    Val
  - Assert
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - AutoTune
    
    FunctionCallMap
    
    FunctionSet
    
    VariableMap
    
    VariableSet
    
    addTypeAttributeVisitor
    
    collectFunctionCallsVisitor
    
    enumVisitor
    
    functionVisitor
    
    modFunctionAnnotatorVisitor
    
    modVisitor
    
    octagonFunctionVisitor
    
    octagonVariableVisitor
  - Base
    
    MainFunctor
    
    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
  - BoolDomain
    
    Bool
    
    MayBool
    
    MustBool
  - CfgTools
    
    CfgEdge
    
    CfgEdgeH
    
    Exceptionless
    
    Infix
    
    Labels
    
    CfgPrinters
    
    NodeStyles
    
    NodeStyles
    
    SCC
  - CilCfg
    
    allBBVisitor
    
    countLoopsVisitor
  - CilMaps
    
    FundecForMap
    
    FundecMap
    
    VarinfoMap
    
    VarinfoOrdered
  - CommonPriv
    
    ConfCheck
    
    RequireMutexActivatedInit
    
    RequireMutexPathSensOneMainInit
    
    RequireThreadFlagPathSensInit
    
    Locksets
    
    Lockset
    
    MinLocksets
    
    MustLockset
    
    MayVars
    
    MustVars
    
    MutexGlobals
    
    V
    
    VGlobal
    
    VMutex
    
    VMutexInits
    
    PerMutexTidCommon
    
    Conf
    
    D
    
    G
    
    GMutex
    
    GThread
    
    L
    
    LD
    
    LLock
    
    LMust
    
    V
    
    W
    
    PerMutexTidCommonArg
    
    Protection
    
    WriteCenteredD
    
    P
    
    W
  - CompareAST
    
    StringMap
  - CompareCFG
    
    NH
  - CompareCIL
    
    GlobalColMap
    
    GlobalMap
    
    VarinfoSet
  - CompilationDatabase
  - ConcDomain
    
    MustThreadSet
    
    ThreadCreation
    
    DirtyExit
    
    DirtyExitNames
    
    ParentThreadSet
    
    UNames
    
    Uniqueness
    
    ThreadSet
    
    ThreadStringSet
  - CondVars
    
    Domain
    
    Spec
  - 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
    
    CurrentVarEqConstrSys
    
    S
    
    Dom
    
    Var
    
    DeadBranchLifter
    
    C
    
    D
    
    G
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    DeadCodeLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    EqConstrSysFromGlobConstrSys
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    EqIncrSolverFromEqSolver
    
    Arg
    
    S
    
    Dom
    
    Var
    
    Sol
    
    S
    
    Dom
    
    Var
    
    FromSpec
    
    Cfg
    
    I
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    GlobConstrSolFromEqConstrSol
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    S2
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    GlobConstrSolFromEqConstrSolBase
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    GlobSolverFromEqSolver
    
    EqSys
    
    Dom
    
    Var
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    Sol
    
    S
    
    Dom
    
    Var
    
    Sol'
    
    Splitter
    
    HashconsContextLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    HashconsLifter
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
    
    V
    
    Increment
    
    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
    
    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
    
    Var2
    
    GV
    
    LV
    
    WidenContextLifterSide
    
    D
    
    DD
    
    M
    
    P
    
    S
    
    C
    
    D
    
    G
    
    P
    
    V
  - ContextUtil
  - 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
    
    D
    
    LockEventPair
    
    MayLockEventPairs
    
    P
    
    V
  - DeadlockDomain
    
    LockEvent
    
    MayLockEvents
  - 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
  - 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
  - EffectWConEq
    
    Make
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - 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
  - FileDomain
    
    Dom
    
    MD
    
    V
    
    Val
  - FileUse
    
    Spec
  - FlagHelper
    
    FlagError
    
    FlagHelper
    
    L
    
    Msg
    
    R
    
    LatticeFlagHelper
    
    L
    
    Msg
    
    R
    
    LatticeFlagHelperArg
  - FloatDomain
    
    F32Interval
    
    F64Interval
    
    FloatArith
    
    FloatDomTupleImpl
    
    FloatDomain
    
    FloatDomainBase
  - FloatOps
    
    CDouble
    
    CFloat
    
    CFloatType
  - 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
  - GoblintDir
  - Graphml
    
    ArgNodeGraphMlWriter
    
    M
    
    N
    
    DeDupGraphMlWriter
    
    M
    
    EnumerateNodeGraphMlWriter
    
    M
    
    GraphMlWriter
    
    StringGraphMlWriter
    
    XmlGraphMlWriter
  - HoareDomain
    
    HoarePO
    
    B
    
    E
    
    MapBot
    
    R
    
    SpecD
    
    Set
    
    B
    
    SetEM
    
    E
    
    SetS
    
    Set_LiftTop
    
    B
    
    N
  - IntDomain
    
    Arith
    
    ArithIkind
    
    B
    
    BISet
    
    BigInt
    
    Booleans
    
    BooleansNames
    
    Congruence
    
    DefExc
    
    Enums
    
    Flat
    
    Base
    
    FlatPureIntegers
    
    Flattened
    
    FlattenedBI
    
    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
    
    OldDomainFacade
    
    Old
    
    PtrDiffIkind
    
    Reverse
    
    Base
    
    S
    
    SOverflow
    
    SOverflowUnlifter
    
    D
    
    Size
    
    Y
    
    Z
  - IntDomainProperties
    
    All
    
    D
    
    Ikind
    
    AllNonAssoc
    
    D
    
    Ikind
    
    IntegerSet
    
    Base
    
    Ikind
    
    OldS
    
    OldSWithIkind
    
    Ikind
    
    S
    
    Valid
    
    AD
    
    Ikind
    
    AF
    
    CD
    
    Base
    
    WithIkind
    
    I
    
    Ik
    
    Ikind
  - IntOps
    
    BigIntOps
    
    BigIntOpsBase
    
    Int32Ops
    
    Int32OpsBase
    
    Int64Ops
    
    Int64OpsBase
    
    IntOps
    
    IntOpsBase
    
    IntOpsDecorator
    
    B
    
    NIntOps
    
    NIntOpsBase
  - Invariant
    
    ExpLat
    
    N
  - InvariantCil
    
    exp_contains_tmp_visitor
    
    exp_is_in_scope_visitor
    
    exp_replace_original_name_visitor
  - JmpBufDomain
    
    ActiveLongjmps
    
    BufferEntry
    
    BufferEntryOrTop
    
    JmpBufSet
    
    JmpBufSetTaint
    
    LocallyModifiedMap
    
    VarSet
    
    NodeSet
  - LibraryDesc
    
    Access
    
    Accesses
    
    MathLifted
    
    MathPrintable
  - LibraryDsl
  - LibraryFunctions
  - LocalFixpoint
    
    Make
    
    D
  - LockDomain
    
    Lockset
    
    Lock
    
    MayLockset
    
    MayLocksetNoRW
    
    Addr
    
    Mutexes
    
    Simple
    
    Symbolic
    
    S
  - LocksetAnalysis
    
    DS
    
    Make
    
    D
    
    MakeMay
    
    A
    
    Arg
    
    D
    
    G
    
    V
    
    D
    
    P
    
    MakeMust
    
    A
    
    Arg
    
    D
    
    G
    
    V
    
    D
    
    P
    
    MayArg
    
    D
    
    G
    
    V
    
    MustArg
    
    D
    
    G
    
    V
  - LoopTermination
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    Statements
  - LoopUnrolling
    
    StatementHashTable
    
    arrayVisitor
    
    checkNoBreakVisitor
    
    copyandPatchLabelsVisitor
    
    findAssignmentConstDiff
    
    findBreakVisitor
    
    hasAssignmentVisitor
    
    isPointedAtVisitor
    
    loopUnrollingCallVisitor
    
    loopUnrollingVisitor
    
    patchLabelsGotosVisitor
  - Lval
    
    Set
  - 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
  - MakefileUtil
  - MallocFresh
    
    Spec
    
    A
    
    D
  - Malloc_null
    
    Spec
    
    P
  - 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
  - MaxIdUtil
  - MayLocks
    
    Arg
    
    D
    
    G
    
    V
    
    Spec
    
    A
    
    D
    
    G
    
    P
    
    V
  - MemLeak
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    ToppedVarInfoSet
  - MemOutOfBounds
    
    Spec
  - ModifiedSinceLongjmp
    
    Spec
  - MusteqDomain
    
    Equ
    
    F
    
    P
    
    VF
  - MutexAnalysis
    
    Spec
    
    A
    
    Arg
    
    D
    
    G
    
    GProtected
    
    GProtecting
    
    MakeP
    
    G0
    
    P
    
    ReadWrite
    
    Write
    
    Multiplicity
    
    Count
    
    V
    
    C
    
    GM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    VarSet
  - MutexAttrDomain
    
    MutexKind
  - MutexEventsAnalysis
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - MutexTypeAnalysis
    
    Spec
    
    A
    
    G
    
    P
    
    V
  - Mval
    
    Exp
    
    Lattice
    
    MakeLattice
    
    Offs
    
    MakePrintable
    
    Offs
    
    Printable
    
    Unit
  - MvalMapDomain
    
    Domain
    
    MD
    
    V
    
    S
    
    Value
    
    Impl
  - 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
  - Offset
    
    Exp
    
    Index
    
    Exp
    
    Printable
    
    Unit
    
    Lattice
    
    MakeLattice
    
    Idx
    
    MakePrintable
    
    Idx
    
    Printable
    
    Unit
  - PartitionDomain
    
    Collapse
    
    CollapseSet
    
    ExpPartitions
    
    B
    
    E
    
    Make
    
    S
    
    Set
    
    S
    
    SetSet
    
    B
    
    Base
    
    E
  - PoisonVariables
    
    Spec
    
    VS
  - PostSolver
    
    Compose
    
    PS1
    
    S
    
    Dom
    
    Var
    
    PS2
    
    EqConstrSysFromStartEqConstrSys
    
    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
  - 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
  - PrecisionUtil
  - 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
  - Queries
    
    Any
    
    ES
    
    FlatYojson
    
    Hashtbl
    
    Exceptionless
    
    Infix
    
    Labels
    
    NFL
    
    Protection
    
    Result
    
    Set
    
    Exceptionless
    
    Labels
    
    TC
    
    TS
    
    ThreadNodeLattice
    
    VI
    
    VS
  - RaceAnalysis
    
    Spec
    
    G
    
    MemoSet
    
    OffsetTrie
    
    ChildMap
    
    Trie
    
    OneOffset
    
    V
  - Refinement
  - Region
    
    Spec
    
    A
    
    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
  - 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
  - Sarif
  - SarifRules
  - SarifType
    
    Artifact
    
    ArtifactLocation
    
    Invocation
    
    Location
    
    Message
    
    PhysicalLocation
    
    Region
    
    ReportingDescriptor
    
    Result
    
    Run
    
    SarifLog
    
    Tool
    
    ToolComponent
  - Selector
    
    Make
    
    Arg
    
    S
    
    Dom
    
    Var
  - Serialize
    
    Cache
  - 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
  - SetDomain
    
    Elements
    
    FiniteSet
    
    E
    
    Elems
    
    FiniteSetElems
    
    HeadlessSet
    
    Base
    
    Joined
    
    E
    
    LiftTop
    
    N
    
    S
    
    Make
    
    Base
    
    Print
    
    E
    
    S
    
    Reverse
    
    Base
    
    S
    
    SensitiveConf
    
    Base
    
    C
    
    Elt
    
    User
    
    ToppedSet
    
    Base
    
    N
    
    ToppedSetNames
  - SharedFunctions
  - Signs
    
    SL
    
    Signs
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - SolverBox
    
    NarrowOption
    
    D
    
    S
    
    D
    
    Warrow
    
    D
    
    Widen
    
    D
  - SolverStats
  - Spec
    
    SC
    
    Spec
    
    SpecCheck
  - SpecDomain
    
    Dom
    
    MD
    
    V
    
    Val
  - StackDomain
    
    Dom1
    
    Var
    
    VarLat
    
    Dom2
    
    Dom3
    
    Loc
    
    S
  - StackTrace
    
    Spec
    
    D
    
    N
    
    Spec1
    
    A
    
    D
    
    P
    
    V
    
    Spec2
    
    A
    
    D
    
    P
    
    V
    
    SpecLoc
  - StructDomain
    
    Arg
    
    FlagConfiguredStructDomain
    
    Val
    
    KeyedSets
    
    Val
    
    S
    
    Sets
    
    Val
    
    Simple
    
    Val
  - Svcomp
    
    Result
    
    StackTaskResult
    
    Arg
    
    Edge
    
    Node
    
    TaskResult
    
    Arg
    
    Node
    
    Task
    
    Cfg
    
    TaskResult
    
    Arg
    
    Edge
    
    Node
  - SvcompSpec
  - SymbLocks
    
    PS
    
    Spec
    
    A
    
    E
  - SymbLocksDomain
    
    Exp
    
    ILock
    
    Idx
    
    LockingPattern
  - Taint
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    VarinfoSet
  - TaintPartialContexts
    
    Spec
    
    VS
  - 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
  - TerminationPreprocessing
    
    VarToStmt
    
    loopCounterVisitor
  - ThreadAnalysis
    
    Spec
    
    P
    
    V
  - ThreadEscape
    
    Spec
    
    ThreadIdSet
  - ThreadFlag
    
    Spec
    
    A
    
    P
  - ThreadFlagDomain
    
    S
    
    Simple
    
    Trivial
  - ThreadId
    
    Spec
    
    A
    
    Created
    
    Callees
    
    Current
    
    D
    
    N
    
    P
    
    VNI
  - ThreadIdDomain
    
    FlagConfiguredTID
    
    D
    
    FunNode
    
    History
    
    Base
    
    D
    
    Lift
    
    Thread
    
    S
    
    Stateful
    
    D
    
    Stateless
    
    ThreadLiftNames
    
    ThreadLifted
    
    Unit
    
    Base
    
    D
  - ThreadJoins
    
    Spec
    
    D
    
    V
  - ThreadReturn
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
  - TimeUtil
  - Timeout
    
    Js
    
    Unix
  - TmpSpecial
    
    Spec
    
    D
    
    Deps
    
    MLDeps
  - 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
  - Transform
    
    PartialEval
    
    visitor
    
    S
  - TrieDomain
    
    Make
    
    ChildMap
    
    Key
    
    Trie
    
    Value
  - UnassumeAnalysis
    
    EH
    
    FH
    
    Spec
    
    D
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
  - Uninit
    
    Spec
    
    P
  - UnionDomain
    
    Arg
    
    Field
    
    S
    
    Simple
    
    Values
  - UnitAnalysis
    
    Spec
  - UpdateCil
  - UseAfterFree
    
    AllocaVars
    
    HeapVars
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    StackAndHeapVars
    
    ThreadIdToJoinedThreadsMap
  - ValueDomain
    
    Addr
    
    Mval
    
    Offs
    
    AddrSetDomain
    
    Blob
    
    Size
    
    Value
    
    Blobs
    
    CArrays
    
    Compound
    
    IndexDomain
    
    InvariantArg
    
    Mval
    
    Offs
    
    S
    
    Structs
    
    Unions
    
    ValueInvariant
    
    Arg
    
    VS
    
    ZeroInit
  - ValueDomainQueries
    
    AD
    
    Addr
    
    ID
    
    LS
  - VarEq
    
    Spec
    
    D
  - VarQuery
  - 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
  - WideningThresholds
  - 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
  - Worklist
    
    Make
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - WrapperFunctionAnalysis
    
    MakeUniqueCount
    
    UniqueCountArgs
    
    MallocUniqueCount
    
    MallocWrapper
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    NodeFlatLattice
    
    SpecBase
    
    D
    
    NodeFlatLattice
    
    UniqueCallCounter
    
    UniqueCount
    
    WrapperArgs
    
    ThreadCreateUniqueCount
    
    ThreadCreateWrapper
    
    A
    
    C
    
    D
    
    G
    
    P
    
    V
    
    UniqueCountArgs
    
    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.sites.dune
- Goblint_sites
goblint.sites.js
- Goblint_sites
goblint.std
- Goblint_std
  - GobFpath
  - GobGc
  - GobHashtbl
  - GobList
    
    Syntax
  - GobOption
    
    Syntax
  - GobPretty
  - GobRef
  - GobResult
    
    Syntax
  - GobSys
  - GobUnix
  - GobYaml
  - GobYojson
  - GobZ
goblint.timing
- Goblint_timing
  - Make
    
    Name
  - Name
  - S

Legend:
Library
Module
Module type
Parameter
Class
Class type

The solver that actually uses the implementation based of GobConfig.get_string "solver".

Parameters

module Arg : Analyses.IncrSolverArg

module S : Analyses.EqConstrSys

module VH : Batteries.Hashtbl.S with type key = S.v

Signature

type marshal = Stdlib.Obj.t

val copy_marshal : marshal -> Stdlib.Obj.t

val relift_marshal : marshal -> Stdlib.Obj.t

val solve : 
  (S.v * S.d) list ->
  S.v list ->
  marshal option ->
  S.d VH.t * Stdlib.Obj.t