package goblint

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package goblint

goblint.lib
- Goblint_lib
  - AbortUnless
    
    Spec
  - AbstractionDomainProperties
    
    AbstractFunction
    
    AbstractTest
    
    AD
    
    CD
    
    Monotone
    
    AD
    
    AF
    
    CD
    
    ValidTest
    
    AD
    
    AF
    
    CD
  - Access
    
    A
    
    AS
    
    LV
    
    LVOpt
    
    O
    
    T
  - AccessAnalysis
    
    Spec
    
    V
  - AccessDomain
    
    Event
    
    EventSet
  - AccessKind
  - AddressDomain
    
    AddressSet
    
    Addr
    
    Offs
    
    R
    
    UnitIdxDomain
    
    Idx
    
    J
    
    ShortAddr
    
    S
  - AfterConfig
  - Analyses
    
    ControlSpecC
    
    DefaultSpec
    
    Dom
    
    LD
    
    EmptyV
    
    EqConstrSys
    
    Dom
    
    Var
    
    GVarF
    
    V
    
    GVarG
    
    C
    
    CSet
    
    G
    
    GenericEqBoxIncrSolver
    
    Arg
    
    S
    
    Dom
    
    Var
    
    GenericEqBoxIncrSolverBase
    
    S
    
    Dom
    
    Var
    
    GenericEqBoxSolver
    
    S
    
    Dom
    
    Var
    
    GenericGlobSolver
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    GlobConstrSys
    
    D
    
    G
    
    GVar
    
    LVar
    
    IdentitySpec
    
    IncrSolverArg
    
    MCPA
    
    MCPSpec
    
    A
    
    C
    
    D
    
    G
    
    V
    
    MonSystem
    
    Dom
    
    Var
    
    Result
    
    C
    
    Exceptionless
    
    Infix
    
    Labels
    
    Range
    
    ResultConf
    
    ResultNode
    
    ResultType2
    
    S
    
    C
    
    D
    
    G
    
    V
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    SpecSysVar
    
    StdV
    
    SysVar
    
    UnitA
    
    Var
    
    VarF
    
    LD
    
    VarType
    
    VarinfoV
  - ApronAnalysis
  - ApronDomain
  - ApronPrecCompareUtil
  - ApronPriv
  - ArrayDomain
    
    AttributeConfiguredArrayDomain
    
    Idx
    
    Val
    
    LatticeWithSmartOps
    
    Partitioned
    
    Idx
    
    Val
    
    PartitionedWithLength
    
    Idx
    
    Val
    
    S
    
    Trivial
    
    Idx
    
    Val
    
    TrivialWithLength
    
    Idx
    
    Val
  - Assert
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - AutoTune
    
    FunctionCallMap
    
    FunctionSet
    
    VariableMap
    
    VariableSet
    
    addTypeAttributeVisitor
    
    collectFunctionCallsVisitor
    
    enumVisitor
    
    functionVisitor
    
    modFunctionAnnotatorVisitor
    
    modVisitor
    
    octagonFunctionVisitor
    
    octagonVariableVisitor
  - AutoTune0
    
    collectComplexityFactorsVisitor
  - Base
    
    MainFunctor
    
    Dom
    
    G
    
    Priv
    
    D
    
    G
    
    V
    
    RVEval
    
    V
    
    VarH
    
    Exceptionless
    
    Infix
    
    Labels
    
    VarMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    MainSpec
    
    A
    
    C
    
    D
    
    G
    
    V
  - BaseDomain
    
    BaseComponents
    
    PrivD
    
    CPA
    
    M
    
    DomFunctor
    
    ExpEval
    
    PrivD
    
    DomWithTrivialExpEval
    
    PrivD
    
    ExpEvaluator
    
    Glob
    
    PartDeps
    
    VarSet
    
    WeakUpdates
  - BasePriv
    
    S
    
    D
    
    G
    
    V
  - BaseUtil
  - Basetype
    
    Bools
    
    CilExp
    
    CilField
    
    CilStmt
    
    ExtractLocation
    
    RawBools
    
    RawStrings
    
    Strings
    
    Variables
  - BoolDomain
    
    Bool
    
    MayBool
    
    MustBool
  - CfgTools
    
    CfgPrinters
    
    NodeStyles
    
    NodeStyles
    
    SCC
  - CilCfg
    
    allBBVisitor
  - CilLval
    
    Set
  - CilMaps
    
    VarinfoMap
    
    VarinfoOrdered
  - 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
    
    StmtH
    
    StringH
    
    VarinfoH
    
    addConstructors
    
    countFnVisitor
  - Cilfacade0
  - CommonPriv
    
    ConfCheck
    
    RequireMutexActivatedInit
    
    RequireMutexPathSensInit
    
    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
    
    GlobalMap
    
    StringMap
  - CompareCFG
    
    NH
  - CompareCIL
    
    VarinfoSet
  - CompilationDatabase
  - ConcDomain
    
    MustThreadSet
    
    ThreadCreation
    
    DirtyExit
    
    DirtyExitNames
    
    ParentThreadSet
    
    UNames
    
    Uniqueness
    
    ThreadSet
    
    ThreadStringSet
  - CondVars
    
    Domain
    
    Spec
  - ConfigProfile
  - ConfigVersion
  - Constants
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - Constraints
    
    CompareEqSys
    
    Compare
    
    CompareD
    
    Var
    
    Sys
    
    Dom
    
    Var
    
    CompareGlobSys
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    C
    
    D
    
    G
    
    V
    
    Sys
    
    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
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    DeadCodeLifter
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    EqConstrSysFromGlobConstrSys
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    EqIncrSolverFromEqSolver
    
    Arg
    
    S
    
    Dom
    
    Var
    
    Sol
    
    S
    
    Dom
    
    Var
    
    FromSpec
    
    Cfg
    
    I
    
    S
    
    C
    
    D
    
    G
    
    V
    
    GlobConstrSolFromEqConstrSol
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    S2
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    GlobConstrSolFromEqConstrSolBase
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    GlobSolverFromEqSolver
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    Sol
    
    S
    
    Dom
    
    Var
    
    HashconsContextLifter
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    HashconsLifter
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    Increment
    
    LevelSliceLifter
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    LimitLifter
    
    C
    
    D
    
    G
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    OptEqual
    
    C
    
    D
    
    G
    
    S
    
    C
    
    D
    
    G
    
    V
    
    V
    
    PathSensitive2
    
    D
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    Var2
    
    GV
    
    LV
    
    WidenContextLifterSide
    
    D
    
    DD
    
    M
    
    S
    
    C
    
    D
    
    G
    
    V
  - ContextUtil
  - Control
    
    AnalyzeCFG
    
    Cfg
    
    CompareGlobSys
    
    G
    
    CSet
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    EQSys
    
    D
    
    G
    
    CSet
    
    GVar
    
    LVar
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Inc
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    LT
    
    PostSolverArg
    
    RT
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    Slvr
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    WResult
    
    S2S
    
    C
    
    D
    
    G
    
    V
    
    X
    
    C
    
    D
    
    G
    
    V
  - Deadlock
    
    Spec
    
    A
    
    Arg
    
    G
    
    V
    
    D
    
    LockEventPair
    
    MayLockEventPairs
    
    V
  - DeadlockDomain
    
    LockEvent
    
    MayLockEvents
  - DisjointDomain
    
    CombinedSet
    
    B
    
    E
    
    RC
    
    Congruence
    
    PairwiseMap
    
    B
    
    C
    
    E
    
    R
    
    PairwiseSet
    
    B
    
    C
    
    E
    
    ProjectiveSet
    
    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
  - Edge
  - EffectWConEq
    
    Make
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - EscapeDomain
    
    EscapedVars
  - EvalAssert
    
    EvalAssert
    
    visitor
  - Events
  - ExpRelation
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - ExpressionEvaluation
    
    ExpEval
  - Expsplit
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - ExtractPthread
    
    Action
    
    Codegen
    
    Action
    
    AdjacencyMatrix
    
    HashtblN
    
    Exceptionless
    
    Infix
    
    Labels
    
    PmlResTbl
    
    FunTbl
    
    Writer
    
    Edges
    
    Env
    
    Resource
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    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
    
    GroupableFlagHelper
    
    L
    
    Msg
    
    R
    
    LatticeFlagHelper
    
    L
    
    Msg
    
    R
    
    LatticeFlagHelperArg
  - FlagModeDomain
    
    Dom
    
    Eq
    
    L_names
    
    Method
    
    P
  - 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
  - GobConfig
    
    Impl
    
    S
    
    Validator
    
    ValidatorRequireAll
  - GobFormat
  - GobFpath
  - GobHashtbl
  - GobList
    
    Syntax
  - GobOption
    
    Syntax
  - GobResult
    
    Syntax
  - GobSys
  - GobUnix
  - GobYaml
  - GobYojson
  - GoblintDir
  - Goblintutil
  - Graphml
    
    ArgNodeGraphMlWriter
    
    M
    
    N
    
    DeDupGraphMlWriter
    
    M
    
    EnumerateNodeGraphMlWriter
    
    M
    
    GraphMlWriter
    
    StringGraphMlWriter
    
    XmlGraphMlWriter
  - HoareDomain
    
    HoarePO
    
    B
    
    E
    
    MapBot
    
    R
    
    SpecD
    
    SpecDGroupable
    
    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
    
    Lift
    
    Base
    
    Lifted
    
    MakeBooleans
    
    Names
    
    OldDomainFacade
    
    Old
    
    PtrDiffIkind
    
    Reverse
    
    Base
    
    S
    
    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
  - 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
    
    ProdConf
    
    Base1
    
    Base2
    
    C
    
    ProdList
    
    Base
    
    N
    
    ProdSimple
    
    Base1
    
    Base2
    
    Reverse
    
    Base
    
    S
    
    Unit
    
    UnitConf
    
    N
  - LazyEval
    
    Make
    
    M
  - LibraryDesc
    
    Access
    
    Accesses
  - LibraryDsl
  - LibraryFunctionEffects
  - LibraryFunctions
  - LockDomain
    
    Glob
    
    Lockset
    
    AddrSet
    
    Lock
    
    ReverseAddrSet
    
    MayLockset
    
    Mutexes
    
    Simple
    
    Symbolic
    
    S
  - LocksetAnalysis
    
    DS
    
    Make
    
    D
    
    MakeMay
    
    A
    
    Arg
    
    D
    
    G
    
    V
    
    D
    
    MakeMust
    
    A
    
    Arg
    
    D
    
    G
    
    V
    
    D
    
    MayArg
    
    D
    
    G
    
    V
    
    MustArg
    
    D
    
    G
    
    V
  - LoopUnrolling
    
    StatementHashTable
    
    arrayVisitor
    
    checkNoBreakVisitor
    
    copyandPatchLabelsVisitor
    
    findAssignmentConstDiff
    
    findBreakVisitor
    
    hasAssignmentVisitor
    
    isPointedAtVisitor
    
    loopUnrollingCallVisitor
    
    loopUnrollingVisitor
    
    patchLabelsGotosVisitor
  - Lval
    
    CilLval
    
    Fields
    
    FI
    
    IdxDomain
    
    IdxPrintable
    
    Normal
    
    Idx
    
    Offs
    
    NormalLat
    
    Idx
    
    Offs
    
    NormalLatRepr
    
    Idx
    
    Offs
    
    R
    
    UnitIdxDomain
    
    Offset
    
    Idx
    
    OffsetPrintable
    
    Idx
    
    S
  - LvalMapDomain
    
    Domain
    
    MD
    
    V
    
    S
    
    Value
    
    Impl
  - MCP
    
    MCP2
  - MCPAccess
    
    A
  - MCPRegistry
    
    AccListSpec
    
    ContextListSpec
    
    DomListLattice
    
    DLSpec
    
    DomListPrintable
    
    DLSpec
    
    DomVariantLattice
    
    DLSpec
    
    DomVariantLattice0
    
    DLSpec
    
    DomVariantPrintable
    
    DLSpec
    
    DomVariantSysVar
    
    DLSpec
    
    DomainListLatticeSpec
    
    DomainListMCPASpec
    
    DomainListPrintableSpec
    
    DomainListSysVarSpec
    
    GlobalDomainListSpec
    
    LocalDomainListSpec
    
    PrintableOfLatticeSpec
    
    D
    
    PrintableOfMCPASpec
    
    D
    
    PrintableOfSysVarSpec
    
    D
    
    VarListSpec
  - MHP
  - MHPAnalysis
    
    Spec
    
    A
  - Maingoblint
  - MakefileUtil
  - MallocFresh
    
    Spec
    
    A
    
    D
  - MallocWrapperAnalysis
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - Malloc_null
    
    Spec
  - 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
    
    S
    
    Timed
    
    M
  - MaxIdUtil
  - MayLocks
    
    Arg
    
    Spec
    
    A
    
    D
    
    G
    
    V
  - MessageCategory
    
    Behavior
    
    Undefined
    
    ArrayOutOfBounds
    
    Cast
    
    Integer
  - MessageUtil
  - Messages
    
    Location
    
    Message
    
    MultiPiece
    
    Piece
    
    Severity
    
    Table
    
    MH
    
    Tag
    
    Tags
  - MusteqDomain
    
    Equ
    
    EquAddr
    
    F
    
    P
  - MutexAnalysis
    
    Spec
    
    A
    
    Arg
    
    G
    
    GProtected
    
    ReadWrite
    
    Write
    
    GProtecting
    
    ReadWrite
    
    Write
    
    MakeG
    
    G0
    
    ReadWrite
    
    Write
    
    V
    
    C
    
    GM
    
    Exceptionless
    
    Infix
    
    Labels
    
    VarSet
  - MutexEventsAnalysis
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    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
    
    Edge
    
    Node
    
    Cfg
    
    StackNode
    
    Node
    
    UnCilLogicIntra
    
    Arg
    
    UnCilTernaryIntra
    
    Arg
  - MyCFG
    
    CfgBackward
    
    CfgBidir
    
    CfgForward
    
    NodeH
    
    Exceptionless
    
    Infix
    
    Labels
  - MyCheck
    
    Arbitrary
    
    Gen
    
    Iter
    
    Shrink
  - Node
  - Node0
  - ObserverAnalysis
    
    MakePathSpec
    
    A
    
    Arg
    
    C
    
    D
    
    G
    
    V
    
    MakeSpec
    
    A
    
    Automaton
    
    C
    
    D
    
    G
    
    V
    
    PathArg
    
    StepObserverAutomaton
  - ObserverAutomaton
    
    KMP
    
    KMPArg
    
    KMPArg
    
    S
  - Options
  - PartitionDomain
    
    Collapse
    
    CollapseSet
    
    ExpPartitions
    
    B
    
    E
    
    Make
    
    S
    
    Set
    
    S
    
    SetSet
    
    B
    
    Base
    
    E
  - 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
  - PreValueDomain
    
    AD
    
    Addr
    
    Offs
    
    R
    
    UnitIdxDomain
    
    J
    
    ShortAddr
    
    Addr
    
    Offs
    
    IndexDomain
  - 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
  - Prelude
    
    All
    
    Incubator
    
    Legacy
    
    Ana
    
    cilPrinter
    
    cilVisitor
    
    defaultCilPrinterClass
    
    descriptiveCilPrinter
    
    descriptiveCilPrinterClass
    
    nopCilVisitor
    
    plainCilPrinterClass
  - Preprocessor
    
    FpathH
    
    Exceptionless
    
    Infix
    
    Labels
  - Printable
    
    Blank
    
    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
    
    ProdConf
    
    Base1
    
    Base2
    
    C
    
    ProdConfiguration
    
    ProdSimple
    
    Base1
    
    Base2
    
    S
    
    Showable
    
    SimplePretty
    
    P
    
    SimpleShow
    
    P
    
    Std
    
    Strings
    
    Unit
    
    UnitConf
    
    N
  - PrivPrecCompareUtil
    
    LV
    
    Util
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
  - ProcessPool
  - PthreadDomain
    
    D
    
    Pred
  - PthreadSignals
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - Queries
    
    Any
    
    ES
    
    Hashtbl
    
    Exceptionless
    
    Infix
    
    Labels
    
    ID
    
    LS
    
    Result
    
    Set
    
    Exceptionless
    
    Labels
    
    TS
    
    VI
  - RaceAnalysis
    
    Spec
    
    G
    
    V
    
    V0
    
    V0Set
  - Refinement
  - Region
    
    Spec
    
    A
    
    Lvals
    
    V
  - RegionDomain
    
    B
    
    RS
    
    Reg
    
    RegMap
    
    RegPart
    
    S
    
    RegionDom
    
    VF
    
    VFB
  - ResettableLazy
  - RichVarinfo
    
    BiVarinfoMap
    
    Collection
    
    Make
    
    X
    
    S
    
    G
    
    H
    
    Make
    
    X
    
    VarinfoMap
  - SLR
    
    JustWiden
    
    D
    
    H
    
    HeapCompare
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    Make
    
    D
    
    H
    
    HeapCompare
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    MyGenericEqBoxSolver
    
    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
    
    D
    
    H
    
    HeapCompare
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    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
    
    Function
    
    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
  - Signs
    
    SL
    
    Signs
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - Spec
    
    Spec
    
    SpecCheck
  - SpecCore
  - SpecDomain
    
    Dom
    
    MD
    
    V
    
    Val
  - SpecLexer
  - SpecParser
  - SpecUtil
  - StackDomain
    
    Dom1
    
    Var
    
    VarLat
    
    Dom2
    
    Dom3
    
    Loc
    
    S
  - StackTrace
    
    Spec
    
    D
    
    P
    
    Spec1
    
    A
    
    D
    
    V
    
    Spec2
    
    A
    
    D
    
    V
    
    SpecLoc
  - StructDomain
    
    Arg
    
    FlagConfiguredStructDomain
    
    Val
    
    KeyedSets
    
    Val
    
    S
    
    Sets
    
    Val
    
    Simple
    
    Val
  - Svcomp
    
    Result
    
    StackTaskResult
    
    Arg
    
    Edge
    
    Node
    
    Cfg
    
    TaskResult
    
    Arg
    
    Edge
    
    Node
    
    Task
    
    Cfg
    
    TaskResult
    
    Arg
    
    Edge
    
    Node
  - SvcompSpec
  - SymbLocks
    
    PS
    
    Spec
    
    A
    
    E
  - SymbLocksDomain
    
    Exp
    
    ILock
    
    Idx
    
    Offs
    
    LockingPattern
  - Taint
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
    
    VarinfoSet
  - Td3
    
    WP
    
    Arg
    
    CurrentVarS
    
    S
    
    Dom
    
    Var
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - Termination
    
    Spec
    
    TermDomain
    
    loopBreaksVisitor
    
    loopCounterVisitor
    
    loopInstrVisitor
    
    loopVarsVisitor
    
    recomputeVisitor
  - ThreadAnalysis
    
    Spec
    
    V
  - ThreadEscape
    
    Spec
  - ThreadFlag
    
    Spec
    
    A
  - ThreadFlagDomain
    
    S
    
    Simple
    
    Trivial
  - ThreadId
    
    Spec
    
    A
    
    D
  - ThreadIdDomain
    
    FlagConfiguredTID
    
    D
    
    FunNode
    
    History
    
    Base
    
    D
    
    Lift
    
    Thread
    
    S
    
    Stateful
    
    D
    
    Stateless
    
    ThreadLiftNames
    
    ThreadLifted
    
    Unit
    
    Base
    
    D
  - ThreadJoins
    
    Spec
    
    V
  - ThreadReturn
    
    Spec
    
    A
    
    C
    
    D
    
    G
    
    V
  - TimeUtil
  - Timeout
    
    Js
    
    Unix
  - Timing
    
    Default
    
    Program
  - 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
  - Tracing
    
    Strs
  - Transform
    
    PartialEval
    
    visitor
    
    S
  - Uninit
    
    Spec
  - UnionDomain
    
    Arg
    
    Field
    
    S
    
    Simple
    
    Values
  - UnitAnalysis
    
    Spec
  - UpdateCil
  - UpdateCil0
    
    NodeMap
  - ValueDomain
    
    AddrSetDomain
    
    Blob
    
    Size
    
    Value
    
    Blobs
    
    CArrays
    
    Compound
    
    InvariantArg
    
    Offs
    
    S
    
    Structs
    
    Unions
    
    ValueInvariant
    
    Arg
    
    VS
    
    ZeroInit
  - VarEq
    
    Spec
    
    D
  - VarQuery
  - Version
  - Violation
    
    Feasibility
    
    Node
    
    PathArg
    
    Node
    
    UnknownFeasibility
    
    Node
    
    ViolationArg
    
    Node
  - ViolationZ3
  - WideningThresholds
  - Witness
    
    Result
    
    Cfg
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    WitnessTaskResult
    
    Arg
    
    Node
  - WitnessConstraints
    
    PathSensitive3
    
    C
    
    D
    
    G
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    V
  - WitnessUtil
    
    File
    
    Invariant
    
    Cfg
    
    File
    
    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
  - XmlUtil
  - YamlWitness
    
    Entry
    
    Make
    
    Cfg
    
    EQSys
    
    FCMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    FMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    File
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Query
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    WitnessInvariant
    
    Query
    
    EQSys
    
    Spec
    
    C
    
    D
    
    G
    
    V
    
    ValidationResult
    
    ChainParams
    
    Validator
    
    EQSys
    
    Locator
    
    ES
    
    Exceptionless
    
    Labels
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Query
    
    Spec
    
    C
    
    D
    
    G
    
    V
  - YamlWitnessType
    
    Certification
    
    Entry
    
    EntryType
    
    FlowInsensitiveInvariant
    
    Invariant
    
    Location
    
    LoopInvariant
    
    LoopInvariantCertificate
    
    Metadata
    
    PreconditionLoopInvariant
    
    PreconditionLoopInvariantCertificate
    
    Producer
    
    Target
    
    Task
goblint.sites.dune
- Goblint_sites
goblint.sites.js
- Goblint_sites
goblint.timing
- Goblint_timing
  - Make
    
    Name
  - Name
  - S

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Spec : Analyses.Spec

module EQSys : 
  Analyses.GlobConstrSys
    with module LVar = Analyses.VarF(Spec.C)
     and module GVar = Analyses.GVarF(Spec.V)
     and module D = Spec.D
     and module G = Analyses.GVarG(Spec.G)(Spec.C)

module LHT : BatHashtbl.S with type key = EQSys.LVar.t

module GHT : BatHashtbl.S with type key = EQSys.GVar.t

Signature

module Locator : sig ... end

module LvarS = Locator.ES

module InvariantParser = WitnessUtil.InvariantParser

module VR = ValidationResult

module Query : sig ... end

val loc_of_location : YamlWitnessType.Location.t -> GoblintCil.Cil.location

val validate : Spec.D.t LHT.t -> EQSys.G.t GHT.t -> GoblintCil.Cil.file -> unit