package goblint

You can search for identifiers within the package.

in-package search v0.2.0

goblint.lib
- AbstractionDomainProperties
  - AbstractFunction
  - AbstractTest
    
    AD
    
    CD
  - Monotone
    
    AD
    
    AF
    
    CD
  - ValidTest
    
    AD
    
    AF
    
    CD
- Access
  - Acc_typHashable
  - Ht
  - HtF
    
    Exceptionless
    
    Infix
    
    Labels
    
    T
  - Ident
  - LSSSet
  - LSSet
  - LabeledString
  - LvalOptHash
    
    Exceptionless
    
    Infix
    
    Labels
  - LvalOptHashable
  - PartAccessResult
  - PartOptHash
    
    Exceptionless
    
    Infix
    
    Labels
  - PartOptHashable
  - TypeHash
    
    Exceptionless
    
    Infix
    
    Labels
- AddressDomain
  - AddressSet
    
    Addr
    
    Offs
    
    B
    
    Idx
  - S
- AfterConfig
- Analyses
  - DefaultSpec
  - Dom
    
    LD
  - EqConstrSys
    
    Dom
    
    Var
  - GenericEqBoxIncrSolver
    
    Arg
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - GenericEqBoxIncrSolverBase
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - GenericEqBoxSolver
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - GenericGlobSolver
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
  - GlobConstrSys
    
    D
    
    G
    
    GVar
    
    LVar
  - IdentitySpec
  - IncrSolverArg
  - MCPSpec
    
    C
    
    D
    
    G
  - MonSystem
    
    Dom
    
    Var
  - Result
    
    C
    
    Exceptionless
    
    Infix
    
    Labels
    
    Range
  - ResultConf
  - ResultNode
  - ResultType2
    
    S
    
    C
    
    D
    
    G
  - Spec
    
    C
    
    D
    
    G
  - Var
  - VarF
    
    LD
  - VarType
- ApronAnalysis
- ApronDomain
- ApronPrecCompareUtil
- ApronPriv
- Arinc
  - Functions
  - Spec
    
    C
    
    D
    
    G
- ArincDomain
  - D
  - Pred
  - Pri
- ArincUtil
  - Action
  - FunTbl
  - GenSig
  - SymTbl
    
    Gen
  - SymTblSig
- ArrayDomain
  - FlagConfiguredArrayDomain
    
    Idx
    
    Val
  - LatticeWithSmartOps
  - Partitioned
    
    Idx
    
    Val
  - PartitionedWithLength
    
    Idx
    
    Val
  - S
  - Trivial
    
    Idx
    
    Val
  - TrivialWithLength
    
    Idx
    
    Val
- Base
  - MainFunctor
    
    Dom
    
    Priv
    
    D
    
    G
    
    RVEval
  - MainSpec
    
    C
    
    D
    
    G
- BaseDomain
  - BaseComponents
    
    PrivD
  - CPA
    
    M
  - DomFunctor
    
    ExpEval
    
    PrivD
  - DomWithTrivialExpEval
    
    PrivD
  - ExpEvaluator
  - Glob
  - PartDeps
    
    VarSet
  - WeakUpdates
- BasePriv
  - S
    
    D
    
    G
- BaseUtil
- Basetype
  - Bools
  - CilExp
  - CilField
  - CilStmt
  - ExtractLocation
  - FieldVariables
  - RawBools
  - RawStrings
  - Strings
  - Variables
- BoolDomain
  - Bool
  - MayBool
  - MustBool
- CfgTools
  - CfgPrinters
    
    NodeStyles
  - NS
  - NodeStyles
  - SCC
- CilType
  - Compinfo
  - Constant
  - Exp
  - Fieldinfo
  - Fundec
  - Location
  - Lval
  - Offset
  - S
  - Std
  - Stmt
  - Typ
  - Varinfo
- Cilfacade
- CommonPriv
- CompareAST
  - GlobalMap
- CompareCFG
  - NH
  - NTH
- CompareCIL
- ConcDomain
- CondVars
  - Domain
  - Spec
- Config
- Constants
  - Spec
    
    C
    
    D
    
    G
- Constraints
  - Compare
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    C
    
    D
    
    G
    
    Sys
  - CompareEq
    
    Compare
    
    CompareD
    
    Sys
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Var
  - DeadCodeLifter
    
    S
    
    C
    
    D
    
    G
  - EqConstrSysFromGlobConstrSys
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
  - EqIncrSolverFromEqSolver
    
    Arg
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    Sol
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - FromSpec
    
    Cfg
    
    I
    
    S
    
    C
    
    D
    
    G
  - GlobConstrSolFromEqConstrSol
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    S2
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - GlobConstrSolFromEqConstrSolBase
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - GlobSolverFromEqSolver
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    Sol
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - HashconsContextLifter
    
    S
    
    C
    
    D
    
    G
  - HashconsLifter
    
    S
    
    C
    
    D
    
    G
  - Increment
  - LevelSliceLifter
    
    S
    
    C
    
    D
    
    G
  - LimitLifter
    
    C
    
    D
    
    G
    
    S
    
    C
    
    D
    
    G
  - OptEqual
    
    C
    
    D
    
    G
    
    S
    
    C
    
    D
    
    G
  - PathSensitive2
    
    D
    
    Spec
    
    C
    
    D
    
    G
  - Var2
    
    GV
    
    LV
  - WidenContextLifterSide
    
    D
    
    DD
    
    M
    
    S
    
    C
    
    D
    
    G
- Contain
  - Spec
    
    D
- ContainDomain
  - ArgSet
  - ClassName
  - ClassNameSet
  - Diff
  - Dom
    
    Danger
    
    InhRel
    
    StringPair
  - FieldSet
  - FieldVars
  - FuncName
  - Globals
  - PrettyField
  - VarName
  - VarNameSet
- ContextUtil
- Control
  - AnalyzeCFG
    
    Cfg
    
    Comp
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    EQSys
    
    D
    
    G
    
    GVar
    
    LVar
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Inc
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    LT
    
    PostSolverArg
    
    RT
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    Slvr
    
    Spec
    
    C
    
    D
    
    G
    
    WResult
  - S2S
    
    C
    
    D
    
    G
    
    X
    
    C
    
    D
    
    G
- Db
- Deadcode
  - Locmap
    
    Exceptionless
    
    Infix
    
    Labels
- Deadlock
  - Spec
- DeadlockDomain
  - Lockset
  - MyLock
- DeadlocksByRaces
  - Spec
- Defaults
- 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
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- EscapeDomain
  - EscapedVars
- Events
- Exp
  - Exp
  - LockingPattern
- ExpDomain
- ExpRelation
  - Spec
    
    C
    
    D
    
    G
- ExpressionEvaluation
  - ExpEval
- Extract_arinc
  - Spec
    
    D
    
    FunTbl
    
    H
    
    G
    
    Pfuns
    
    Pids
    
    Pred
    
    Prios
    
    Res
    
    SymTbl
    
    G
    
    Tasks
- Extract_osek
  - Spec
    
    D
    
    FunTbl
    
    H
    
    G
    
    Pfuns
    
    Pids
    
    Pred
    
    Prios
    
    Res
    
    SymTbl
    
    G
    
    Tasks
- FileDomain
  - Dom
    
    MD
    
    V
  - Val
- FileUse
  - Spec
- Flag
  - Spec
    
    VSet
- FlagModeDomain
  - Dom
  - Eq
  - L_names
  - Method
  - P
- FlagModes
  - Spec
- Generic
  - DirtyBoxSolver
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - LoadRunIncrSolver
    
    Arg
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - LoadRunSolver
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - PreciseSideEffectBoxSolver
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - SolverInteractiveWGlob
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    D
    
    G
    
    GVar
    
    LVar
    
    SSH
    
    Exceptionless
    
    Infix
    
    Labels
  - SolverStats
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - SoundBoxSolver
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
  - SoundBoxSolverImpl
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
- GobConfig
  - Impl
  - S
- GobFormat
- GobYojson
- Goblintutil
- Graphml
  - ArgNodeGraphMlWriter
    
    M
    
    N
  - DeDupGraphMlWriter
    
    M
    
    Node
  - EnumerateNodeGraphMlWriter
    
    M
    
    N
  - GraphMlWriter
  - StringGraphMlWriter
  - XmlGraphMlWriter
- HoareDomain
  - HoarePO
    
    B
    
    E
  - MapBot
    
    R
    
    SpecD
    
    SpecDGroupable
  - Set
    
    B
  - SetS
  - Set_LiftTop
    
    B
    
    N
- IntDomain
  - Arith
  - ArithIkind
  - B
  - 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
  - AF
    
    AD
  - All
    
    D
  - AllNonAssoc
    
    D
  - IntegerSet
    
    Base
  - OldS
  - S
  - Valid
    
    AD
  - WithIkind
    
    I
    
    Ik
- IntOps
  - BigIntOps
  - BigIntOpsBase
  - Int32Ops
  - Int32OpsBase
  - Int64Ops
  - Int64OpsBase
  - IntOps
  - IntOpsBase
  - IntOpsDecorator
    
    B
  - NIntOps
  - NIntOpsBase
- Invariant
- InvariantCil
  - exp_is_in_scope_visitor
  - exp_replace_original_name_visitor
- JsonSchema
- Lattice
  - Chain
    
    P
  - Fake
    
    Base
  - FakeSingleton
    
    Base
  - Flat
    
    Base
    
    N
  - HConsed
    
    Base
    
    HC
  - HashCached
    
    LazyHash
    
    M
  - LexProd
    
    Base1
    
    Base2
  - Lift
    
    Base
    
    N
  - Lift2
    
    Base1
    
    Base2
    
    N
  - LiftBot
    
    Base
  - LiftPO
    
    Base
    
    N
  - LiftTop
    
    Base
  - Liszt
    
    Base
  - PD
  - PO
  - Prod
    
    Base1
    
    Base2
  - Prod3
    
    Base1
    
    Base2
    
    Base3
  - ProdConf
    
    Base1
    
    Base2
    
    C
  - ProdSimple
    
    Base1
    
    Base2
  - Reverse
    
    Base
  - S
  - Unit
  - UnitConf
    
    N
- LazyEval
  - Make
    
    M
- LibraryFunctions
- ListDomain
  - S
  - SimpleList
    
    Base
- LockDomain
  - Glob
  - Lockset
    
    AddrSet
    
    Lock
    
    L
    
    ReverseAddrSet
  - MayLockset
  - Mutexes
  - OsekGlob
  - Simple
  - Symbolic
    
    S
- Lval
  - CilLval
  - Fields
    
    FI
  - Normal
    
    Idx
    
    Offs
  - NormalLat
    
    Idx
    
    Offs
  - Offset
    
    Idx
  - S
  - Stateless
    
    Idx
- LvalMapDomain
  - Domain
    
    MD
    
    V
  - S
  - Value
    
    Impl
- MCP
- Maingoblint
- MakefileUtil
- MallocWrapperAnalysis
  - Spec
    
    C
    
    D
    
    G
- Malloc_null
  - Spec
- MapDomain
  - Groupable
  - HConsed
    
    M
  - HashCached
    
    M
  - LiftBot
    
    M
    
    Range
  - LiftTop
    
    M
    
    Range
  - MapBot
    
    Domain
    
    Range
  - MapBot_LiftTop
    
    Domain
    
    Range
  - MapTop
    
    Domain
    
    Range
  - MapTop_LiftBot
    
    Domain
    
    Range
  - PMap
    
    Domain
    
    Range
  - PS
  - S
  - Timed
    
    M
- MayLocks
  - Spec
- MemoryDomain
  - Stack
    
    Map
    
    VD
- MessageCategory
  - Behavior
    
    Undefined
    
    ArrayOutOfBounds
  - Cast
  - Integer
- MessageUtil
- Messages
  - Message
  - MultiPiece
  - Piece
  - Severity
  - Table
    
    MH
  - Tag
  - Tags
- MusteqDomain
  - Equ
  - EquAddr
  - P
- MutexAnalysis
  - MakeSpec
    
    P
    
    G
  - MyParam
  - Spec
    
    G
  - SpecParam
    
    G
  - WriteBased
    
    G
    
    GReadWrite
    
    GWrite
- MyARG
  - CFGEdge
  - CfgIntra
    
    Cfg
  - Edge
  - InlineEdge
  - 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
- MyLiveness
- Node
- ObserverAnalysis
  - MakePathSpec
    
    Arg
    
    C
    
    D
    
    G
  - MakeSpec
    
    Automaton
    
    C
    
    D
    
    G
  - PathArg
  - StepObserverAutomaton
- ObserverAutomaton
  - KMP
    
    KMPArg
  - KMPArg
  - S
- Octagon
  - Spec
    
    C
    
    D
    
    G
- OctagonDomain
  - ArrayOctagon
  - IKind
  - INV
  - S
- OctagonMapDomain
  - ConstraintType
  - E
    
    F
  - MapOctagon
  - MapOctagonBot
  - MatrixCache
    
    L
  - OctLiszt
  - S
  - VD
- Oil
- OilLexer
- OilParser
- OilUtil
- Osek
  - Flag
  - Spec
    
    Acc
    
    Exceptionless
    
    Infix
    
    Labels
    
    AccKeySet
    
    Exceptionless
    
    Labels
    
    AccLoc
    
    AccValSet
    
    Exceptionless
    
    Labels
    
    M
    
    G
    
    MyParam
    
    OffsMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    OffsSet
    
    Exceptionless
    
    Labels
- Osektransactionality
  - Spec
    
    D
- Osektupel
- PartitionDomain
  - Collapse
  - CollapseSet
  - ExpPartitions
    
    B
    
    E
  - Make
    
    S
  - Set
    
    S
  - SetSet
    
    B
    
    Base
    
    E
- Pml
  - Chan
  - Macro
- Pml_arinc
- Pml_osek
- PostSolver
  - Compose
    
    PS1
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    PS2
  - EqConstrSysFromStartEqConstrSys
    
    S
    
    Dom
    
    Var
  - F
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - ListArgFromStdArg
    
    Arg
    
    M
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - Make
    
    PS
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - MakeList
    
    Arg
    
    M
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - MakeListArg
    
    M
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - MakeStdArg
  - Prune
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - S
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - SaveRun
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - StartEqConstrSys
    
    Dom
    
    Var
  - Unit
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - Verify
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
  - Warn
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
- PreValueDomain
  - AD
    
    Addr
    
    Offs
    
    B
  - Addr
    
    Offs
  - IndexDomain
- PrecCompare
  - Comparison
  - Make
    
    D
  - MakeDump
    
    CompareDump
    
    CompareD
    
    Util
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
  - MakeHashtbl
    
    CompareD
    
    D
    
    K
    
    KH
    
    Exceptionless
    
    Infix
    
    Labels
- PrecCompareUtil
  - LocalizedPrintable
  - R
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
  - S
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
  - Util
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
- Prelude
  - All
    
    Incubator
    
    Legacy
  - Ana
    
    cilPrinter
    
    cilVisitor
    
    defaultCilPrinterClass
    
    descriptiveCilPrinter
    
    descriptiveCilPrinterClass
    
    nopCilVisitor
    
    plainCilPrinterClass
- Printable
  - Blank
  - Chain
    
    P
  - ChainParams
  - DefaultNames
  - Either
    
    Base1
    
    Base2
  - HConsed
    
    Base
    
    HC
  - HashCached
    
    LazyHash
    
    M
  - Lift
    
    Base
    
    N
  - Lift2
    
    Base1
    
    Base2
    
    N
  - LiftBot
    
    Base
  - LiftTop
    
    Base
  - LiftingNames
  - Liszt
    
    Base
  - Name
  - Option
    
    Base
    
    N
  - PrintSimple
    
    P
  - Prod
    
    Base1
    
    Base2
  - Prod3
    
    Base1
    
    Base2
    
    Base3
  - ProdConf
    
    Base1
    
    Base2
    
    C
  - ProdConfiguration
  - ProdSimple
    
    Base1
    
    Base2
  - S
  - Showable
  - Std
  - Strings
  - Unit
  - UnitConf
    
    N
- Printer
  - debugCilPrinterClass
- PrivPrecCompareUtil
  - LV
  - Util
    
    Dom
    
    Key
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
- Queries
  - Any
  - ES
  - ID
  - LS
  - Result
  - TS
  - VI
- Refinement
- Region
  - Spec
- RegionDomain
  - B
  - RS
  - Reg
  - RegMap
  - RegPart
    
    S
  - RegionDom
  - VF
  - VFB
- RichVarinfo
  - BiVarinfoMap
    
    Collection
    
    Make
    
    X
    
    S
  - G
  - H
  - Make
    
    X
  - VarinfoMap
- 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
  - MyGenericEqBoxSolver
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    X
  - PrintInfluence
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    S1
    
    X
    
    Sol
    
    H
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    X
  - SLR3
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
  - TwoPhased
    
    D
    
    H
    
    HeapCompare
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    L
    
    P
    
    S
    
    Dom
    
    Var
    
    T
    
    V
    
    X
    
    XY
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
  - Version
- SLRphased
  - Make
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- SLRterm
  - SLR3term
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    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
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
- Serialize
- SetDomain
  - Blank
  - HeadlessSet
    
    Base
  - LiftTop
    
    N
    
    S
  - Make
    
    Base
  - Reverse
    
    Base
  - S
  - Sensitive
    
    Base
    
    Elt
    
    User
  - SensitiveConf
    
    Base
    
    C
    
    Elt
    
    User
  - ToppedSet
    
    Base
    
    N
  - ToppedSetNames
- ShapeDomain
  - Dom
  - Edges
  - ListPtr
    
    AdrPair
  - ListPtrSet
  - ListPtrSetR
  - Offs
  - Rhs
  - SHMap
- Shapes
  - Spec
    
    C
    
    D
    
    G
- Signs
  - SL
  - Signs
  - Spec
    
    C
    
    D
    
    G
- 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
    
    D
  - Spec2
    
    D
  - SpecLoc
- StructDomain
  - S
  - Simple
    
    Val
- Svcomp
  - Result
  - Specification
  - StackTaskResult
    
    Arg
    
    Edge
    
    Node
    
    Cfg
    
    TaskResult
    
    Arg
    
    Edge
    
    Node
  - Task
    
    Cfg
  - TaskResult
    
    Arg
    
    Edge
    
    Node
- SymbLocks
  - PS
  - Spec
    
    ExpSet
    
    Exceptionless
    
    Labels
- Td3
  - WP
    
    Arg
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    Post
    
    S
    
    Dom
    
    Var
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- Termination
- ThreadAnalysis
  - Spec
  - StartLocIDs
- ThreadEscape
  - Spec
- ThreadFlag
  - Spec
- ThreadFlagDomain
  - S
  - Simple
  - Trivial
- ThreadId
  - Spec
    
    D
- ThreadIdDomain
  - FunLoc
  - History
    
    Base
    
    D
  - Lift
    
    Thread
  - S
  - Stateful
    
    D
  - Stateless
  - Thread
    
    D
  - ThreadLiftNames
  - ThreadLifted
  - Unit
    
    Base
    
    D
- ThreadJoins
  - Spec
- ThreadReturn
  - Spec
    
    C
    
    D
    
    G
- TimeUtil
- Timeout
  - Js
  - Unix
- TopDown
  - WP
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- TopDown_deprecated
  - TD3
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- TopDown_space_cache_term
  - WP
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- TopDown_term
  - WP
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    P
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- Tracing
  - Strs
- Transform
  - PartialEval
    
    visitor
  - S
- Uninit
  - Spec
- UnionDomain
  - Field
  - Simple
    
    Values
- Unit
  - Spec
    
    C
    
    D
    
    G
- UpdateCil
  - NodeMap
- ValueDomain
  - AddrSetDomain
  - Blob
    
    Size
    
    Value
  - Blobs
  - CArrays
  - Compound
  - Lists
  - Offs
  - S
  - Structs
  - Unions
  - ZeroInit
- VarEq
  - Spec
    
    D
- Version
- VersionLookup
- Violation
  - Feasibility
    
    Node
  - PathArg
    
    Node
  - UnknownFeasibility
    
    Node
  - ViolationArg
    
    Node
- ViolationZ3
- Witness
  - Result
    
    Cfg
    
    EQSys
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Spec
    
    C
    
    D
    
    G
  - WitnessTaskResult
    
    Arg
    
    Node
- WitnessConstraints
  - Edge
  - N
  - Node
  - PathSensitive3
    
    C
    
    D
    
    G
    
    Spec
    
    C
    
    D
    
    G
- WitnessUtil
  - HashedList
    
    M
  - HashedPair
    
    M1
    
    M2
  - NH
  - NS
- Worklist
  - Make
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Dom
    
    Var
    
    VS
    
    Exceptionless
    
    Labels
- XmlUtil
goblint.sites.dune
- Goblint_sites
goblint.sites.js
- Goblint_sites

Legend:
Library
Module
Module type
Parameter
Class
Class type

Top down solver.

module WP
  (S : Analyses.EqConstrSys)
  (HM : Prelude.Hashtbl.S with type key = S.v) : 
  sig ... end