package goblint

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Libraries

package goblint

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

goblint 1.1.1

Libraries

This package provides the following libraries (via ocamlobjinfo):

goblint.lib

Documentation:

XmlUtil
AfterConfig
Invariant
LazyEval
MyCheck
Printable Some things are not quite lattices ...
CilType
Config System configuration
GobYojson
Prelude
JsonSchema A simpler schema than http://json-schema.org
Tracing
GobConfig New, untyped, path-based configuration subsystem.
MessageUtil
GobFormat
IntOps
Timeout
Goblintutil Globally accessible flags and utility functions.
MessageCategory
Messages
OilUtil
Printer
Cilfacade Helpful functions for dealing with Cil.
Lattice The lattice signature and simple functors for building lattices.
SetDomain
Access
Edge
Node
MyCFG Our Control-flow graph implementation.
RichVarinfo
Basetype
MapDomain Specification and functors for maps.
HoareDomain Abstract domains with Hoare ordering.
IntDomain Abstract Domains for integers. These are domains that support the C * operations on integer values.
InvariantCil
Lval
AddressDomain
BoolDomain
CfgTools
CompareAST
CompareCFG
CompareCIL
Serialize
VersionLookup
UpdateCil
ThreadIdDomain
ConcDomain
Exp
ExpDomain
WitnessUtil
MyARG
PreValueDomain
Queries Structures for the querying subsystem.
ArrayDomain
EscapeDomain
ListDomain
MusteqDomain
StructDomain Abstract domains representing structs.
UnionDomain
ValueDomain
LockDomain
Events
SarifRules
SarifType
Version
Sarif
Analyses Signatures for analyzers, analysis specifications, and result output.
ContextUtil
Defaults Default values for GobConfig-style configuration.
LibraryFunctions This allows us to query information about library functions.
PostSolver
PrecCompareUtil
PrecCompare
Constraints How to generate constraints for a solver using specifications described in Analyses.
Generic
Selector
Worklist
WitnessConstraints An analysis specification for witnesses.
Graphml
MCP Master Control Program
ObserverAutomaton
ObserverAnalysis
Refinement
Svcomp
TimeUtil
Violation
ViolationZ3
Witness
PartitionDomain Partitioning domains.
VarEq Variable equalities necessary for per-element patterns.
Unit Unit values.
BaseDomain domain of the base analysis
ThreadEscape Variables that escape threads using the last argument from pthread_create.
BaseUtil
ThreadFlagDomain
ThreadFlag Multi-threadedness analysis.
CommonPriv
PrivPrecCompareUtil
ThreadId Current thread ID analysis.
BasePriv
Deadcode
ThreadReturn Thread returning analysis.
Base Value analysis.
Uninit Local variable initialization analysis.
Transform
TopDown_term Top down solver.
TopDown_space_cache_term Terminating top down solver that only keeps values at widening points and restores other values afterwards.
TopDown_deprecated
TopDown Top down solver using box/warrow. This is superseded by td3 but kept as a simple version without term & space (& incremental).
ThreadJoins
ThreadAnalysis Thread creation and uniqueness analyses.
Termination Termination of loops.
Td3 Incremental terminating top down solver that optionally only keeps values at widening points and restores other values afterwards.
SymbLocks Symbolic lock-sets for use in per-element patterns.
StackDomain
StackTrace Stack-trace "analyses".
SpecCore
SpecParser
SpecLexer
SpecUtil
LvalMapDomain
SpecDomain
Spec Analysis by specification file.
Signs An analysis specification for didactic purposes.
MyLiveness
RegionDomain
Region Assigning static regions to dynamic memory.
ShapeDomain
Shapes Shape analysis for cyclic doubly linked lists.
SLR The 'slr*' solvers.
SLRterm
SLRphased
Pml
Pml_osek
Pml_arinc
Osektupel
FlagModeDomain
FlagModes Flag state values.
MutexAnalysis Data race analysis.
OilParser
OilLexer
Osek Data race analysis for OSEK programs.
Osektransactionality Another OSEK analysis.
Oil
OctagonDomain
OctagonMapDomain
Octagon
MemoryDomain
MayLocks May-lockset analysis.
Malloc_null Path-sensitive analysis that verifies checking the result of the malloc function.
MallocWrapperAnalysis An analysis that handles the case when malloc is called from a wrapper function all over the code.
MakefileUtil
DomainProperties
Control An analyzer that takes the CFG from MyCFG, a solver from Selector, constraints from Constraints (using the specification from MCP)
Maingoblint This is the main program!
AbstractionDomainProperties
IntDomainProperties
Flag Analysis for the OSEK flag pattern.
FileDomain
FileUse An analysis for checking correct use of file handles.
Extract_osek Extract osek function calls.
ArincDomain
Extract_arinc Extract function calls and variables.
ExpressionEvaluation
ExpRelation An analysis specification to answer questions about how two expressions relate to each other.
EffectWConEq
DeadlocksByRaces Deadlock analysis using data race detection.
DeadlockDomain
Deadlock Deadlock analysis.
Db
ContainDomain
Contain Protection using 'private' field modifier in C++. see doi.org/10.1007/978-3-642-28891-3_11 A. Herz, and K. Apinis "Class-Modular, class-escape and points-to analysis for object-oriented languages" Builds on the ability of LLVM < 3.1 to emit semantically equivalent C code as a target Requires a CXX.json file to work
Constants
CondVars Must equality between variables and logical expressions.
ArincUtil
Arinc Tracking of arinc processes and their actions. Output to console, graphviz and promela.
ApronPriv
ApronPrecCompareUtil
ApronDomain
ApronAnalysis

goblint.sites.dune

Documentation:

Goblint_sites

goblint.sites.js

Documentation:

Goblint_sites