package goblint

You can search for identifiers within the package.

in-package search v0.2.0

goblint index
- CHANGELOG
- README
- Library goblint.backtrace
  - Goblint_backtrace
- Library goblint.build-info
  - Goblint_build_info
- Library goblint.common
  - AnalysisState
  - AnalysisStateUtil
  - Basetype
    
    Variables
    
    RawStrings
    
    CilExp
    
    CilStmt
    
    CilField
  - CfgTools
    
    H
    
    NH
    
    SCC
    
    CfgPrinters
    
    NodeStyles
    
    CfgPrinters
  - CilCfg0
    
    allBBVisitor
  - CilLocation
  - CilType
    
    S
    
    Std
    
    Location
    
    Ikind
    
    Fkind
    
    Unop
    
    Binop
    
    Wstring_type
    
    Encoding
    
    Varinfo
    
    Fundec
    
    Compinfo
    
    Fieldinfo
    
    Enuminfo
    
    Typeinfo
    
    Stmt
    
    Typ
    
    Typsig
    
    Constant
    
    Offset
    
    Lval
    
    Exp
    
    Attrparam
    
    Attribute
    
    Attributes
  - Cilfacade
    
    E
    
    cleanCilPrinterClass
    
    addConstructors
    
    countFnVisitor
    
    StmtH
    
    VarinfoH
    
    StringH
    
    IntH
    
    stmtSidVisitor
    
    FunLocH
    
    LocSet
  - Cilfacade0
  - ContextUtil
  - ControlSpecC
  - Edge
  - FloatOps
    
    CFloatType
    
    CDouble
    
    CFloat
  - GobFormat
  - IntOps
    
    IntOpsBase
    
    IntOps
    
    NIntOpsBase
    
    Int32OpsBase
    
    Int64OpsBase
    
    BigIntOpsBase
    
    IntOpsDecorator
    
    BigIntOps
    
    NIntOps
    
    Int32Ops
    
    Int64Ops
  - LazyEval
    
    Make
  - LoopUnrolling0
    
    CopyOfHashTable
  - MessageCategory
    
    Behavior
    
    Undefined
    
    ArrayOutOfBounds
    
    Integer
    
    Cast
  - MessageUtil
  - Messages
    
    Pretty
    
    Category
    
    Severity
    
    Location
    
    Piece
    
    MultiPiece
    
    Tag
    
    Tags
    
    Message
    
    Table
    
    MH
    
    Strs
  - MyCFG
    
    CfgBackward
    
    CfgForward
    
    CfgBidir
    
    CfgEdge
    
    CfgEdgeH
    
    Exceptionless
    
    Infix
    
    Labels
    
    CfgBidirSkip
    
    NodeH
    
    Exceptionless
    
    Infix
    
    Labels
    
    FileCfg
    
    Cfg
  - Node
  - Node0
  - Printable
    
    Pretty
    
    S
    
    Empty
    
    Std
    
    StdLeaf
    
    Showable
    
    SimpleShow
    
    Prettyable
    
    SimplePretty
    
    Formatable
    
    SimpleFormat
    
    Name
    
    UnitConf
    
    Unit
    
    HConsed
    
    HC
    
    HashCached
    
    LazyHash
    
    PrefixNameConf
    
    PrefixName
    
    LiftConf
    
    DefaultConf
    
    LiftConf
    
    EitherConf
    
    EitherConf
    
    Either
    
    Either3Conf
    
    Either3Conf
    
    Either3
    
    Option
    
    Lift2Conf
    
    Lift2Conf
    
    ProdConfiguration
    
    ProdConf
    
    Prod
    
    ProdSimple
    
    Prod3
    
    PQueue
    
    Liszt
    
    ChainParams
    
    Chain
    
    LiftBot
    
    LiftTop
    
    Strings
    
    FailwithMessage
    
    Failwith
    
    Yojson
    
    Z
  - ResettableLazy
  - RichVarinfo
    
    VarinfoMap
    
    G
    
    H
    
    Make
    
    BiVarinfoMap
    
    S
    
    Collection
    
    Make
  - Timing
    
    Default
    
    Program
  - UpdateCil0
    
    NodeMap
  - XmlUtil
- Library goblint.config
  - AfterConfig
  - GobConfig
    
    Validator
    
    ValidatorRequireAll
    
    S
    
    Impl
  - JsonSchema
    
    JS
    
    JE
    
    JQ
    
    Schema
    
    Validator
  - Options
- Library goblint.constraint
  - Goblint_constraint
    
    ConstrSys
    
    SysVar
    
    VarType
    
    Var2
    
    EqConstrSys
    
    Var
    
    Dom
    
    DemandEqConstrSys
    
    Var
    
    Dom
    
    GlobConstrSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    DemandGlobConstrSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    CurrentVarDemandEqConstrSys
    
    S
    
    Var
    
    Dom
    
    SolverTypes
    
    GenericEqSolver
    
    DemandEqSolver
    
    GenericEqIncrSolverBase
    
    IncrSolverArg
    
    GenericEqIncrSolver
    
    DemandEqIncrSolverBase
    
    DemandEqIncrSolver
    
    DemandGlobIncrSolver
    
    Translators
    
    EqConstrSysFromDemandConstrSys
    
    Var
    
    Dom
    
    EqConstrSysFromGlobConstrSys
    
    Var
    
    Dom
    
    GlobConstrSolFromEqConstrSolBase
    
    GlobConstrSolFromEqConstrSol
    
    S2
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    DemandEqIncrSolverFromGenericEqIncrSolver
    
    GlobSolverFromEqSolver
    
    EqSys
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Sol'
    
    Splitter
    
    VarQuery
- Library goblint.domain
  - BoolDomain
    
    Names
    
    MakeBool
    
    StdNames
    
    Bool
    
    MakeMayBool
    
    MayBool
    
    MustBool
    
    FlatBool
  - DisjointDomain
    
    Representative
    
    ProjectiveSet
    
    MayEqualSetDomain
    
    ProjectiveSetPairwiseMeet
    
    Congruence
    
    PairwiseSet
    
    RepresentativeCongruence
    
    CombinedSet
    
    ProjectiveMap
    
    PairwiseMap
  - FlagHelper
    
    FlagError
    
    FlagHelper
    
    LatticeFlagHelperArg
    
    LatticeFlagHelper
  - HoareDomain
    
    Pretty
    
    HoarePO
    
    Map
    
    B
    
    SetS
    
    Set
    
    Set_LiftTop
    
    MapBot
    
    SetEM
  - Lattice
    
    Pretty
    
    PO
    
    Bot
    
    Top
    
    S
    
    UnitConf
    
    Unit
    
    NoBotTop
    
    Fake
    
    PD
    
    FakeSingleton
    
    Reverse
    
    HConsed
    
    HC
    
    HashCached
    
    LazyHash
    
    FlatConf
    
    Flat
    
    LiftConf
    
    Lift
    
    Lift2Conf
    
    Lift2
    
    ProdConf
    
    Prod
    
    ProdSimple
    
    Prod3
    
    LiftBot
    
    LiftTop
    
    Liszt
    
    Num
    
    ProdList
    
    Chain
  - MapDomain
    
    Pretty
    
    PS
    
    S
    
    Bindings
    
    Print
    
    Groupable
    
    PrintGroupable
    
    Group
    
    GroupMap
    
    PMap
    
    HashCached
    
    HConsed
    
    Timed
    
    MapBot
    
    MapTop
    
    LiftTop
    
    MapBot_LiftTop
    
    LiftBot
    
    MapTop_LiftBot
    
    Joined
  - PartitionDomain
    
    Collapse
    
    Set
    
    CollapseSet
    
    Make
    
    S
    
    SetSet
    
    B
    
    E
    
    ExpPartitions
    
    B
    
    E
  - SetDomain
    
    Pretty
    
    S
    
    Elements
    
    Print
    
    Make
    
    SensitiveConf
    
    Elt
    
    ToppedSetNames
    
    LiftTop
    
    ToppedSet
    
    HeadlessSet
    
    Reverse
    
    FiniteSetElem
    
    FiniteSet
    
    E
    
    Joined
  - TrieDomain
    
    Make
    
    Trie
    
    ChildMap
- Library goblint.incremental
  - CilMaps
    
    FundecForMap
    
    FundecMap
    
    VarinfoOrdered
    
    VarinfoMap
  - CompareAST
    
    StringMap
  - CompareCFG
    
    StringMap
    
    NH
  - CompareCIL
    
    StringMap
    
    NH
    
    FundecForMap
    
    FundecMap
    
    VarinfoOrdered
    
    VarinfoMap
    
    GlobalMap
    
    GlobalColMap
    
    VarinfoSet
  - MakefileUtil
  - MaxIdUtil
  - Serialize
    
    Cache
  - UpdateCil
    
    NodeMap
- Library goblint.lib
  - Goblint_lib
    
    Maingoblint
    
    Control
    
    S2S
    
    AnalyzeCFG
    
    SpecSys
    
    Spec
    
    EQSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    PostSolverArg
    
    Slvr
    
    EqSys
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Sol'
    
    Splitter
    
    CompareGlobSys
    
    Sys
    
    LVar
    
    GVar
    
    D
    
    G
    
    CSet
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    GH
    
    Exceptionless
    
    Infix
    
    Labels
    
    G
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    RT
    
    LT
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    Query
    
    Server
    
    InvariantParser
    
    VarQuery
    
    ArgWrapper
    
    Arg
    
    Node
    
    Edge
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    Request
    
    Registry
    
    ParamParser
    
    Function
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    Node
    
    Edge
    
    MyCFG
    
    CfgTools
    
    Analyses
    
    M
    
    Var
    
    VarF
    
    SpecSysVar
    
    GVarF
    
    GVarFC
    
    GVarG
    
    CSet
    
    Dom
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    Spec2Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    MCPA
    
    MCPSpec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    StdV
    
    UnitV
    
    VarinfoV
    
    EmptyV
    
    UnitA
    
    EmptyP
    
    UnitP
    
    IdentityP
    
    DefaultSpec
    
    G
    
    V
    
    P
    
    A
    
    IdentitySpec
    
    G
    
    V
    
    P
    
    A
    
    IdentityUnitContextsSpec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    ValueContexts
    
    C
    
    SpecSys
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    EQSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    SpecSysSol
    
    SpecSys
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    EQSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Constraints
    
    Increment
    
    FromSpec
    
    LVar
    
    GVar
    
    D
    
    G
    
    CompareConstraints
    
    CompareGlobSys
    
    Sys
    
    LH
    
    GH
    
    G
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    CompareHashtbl
    
    Var
    
    CompareD
    
    CompareEqSys
    
    Compare
    
    Var
    
    CompareD
    
    CompareGlobal
    
    Compare
    
    Var
    
    CompareD
    
    CompareNode
    
    Node
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Compare
    
    Var
    
    CompareD
    
    AnalysisState
    
    AnalysisStateUtil
    
    ControlSpecC
    
    MCP
    
    DomainListPrintableSpec
    
    DomainListRepresentativeSpec
    
    DomainListSysVarSpec
    
    DomainListMCPASpec
    
    DomainListLatticeSpec
    
    PrintableOfLatticeSpec
    
    PrintableOfRepresentativeSpec
    
    PrintableOfMCPASpec
    
    PrintableOfSysVarSpec
    
    DomListPrintable
    
    DomVariantPrintable
    
    DomVariantSysVar
    
    DomListRepresentative
    
    DomListLattice
    
    DomVariantLattice0
    
    DomVariantLattice
    
    LocalDomainListSpec
    
    GlobalDomainListSpec
    
    ContextListSpec
    
    VarListSpec
    
    AccListSpec
    
    PathListSpec
    
    MCP2
    
    D
    
    G
    
    C
    
    V
    
    P
    
    MCPRegistry
    
    DomainListPrintableSpec
    
    DomainListRepresentativeSpec
    
    DomainListSysVarSpec
    
    DomainListMCPASpec
    
    DomainListLatticeSpec
    
    PrintableOfLatticeSpec
    
    PrintableOfRepresentativeSpec
    
    PrintableOfMCPASpec
    
    PrintableOfSysVarSpec
    
    DomListPrintable
    
    DomVariantPrintable
    
    DomVariantSysVar
    
    DomListRepresentative
    
    DomListLattice
    
    DomVariantLattice0
    
    DomVariantLattice
    
    LocalDomainListSpec
    
    GlobalDomainListSpec
    
    ContextListSpec
    
    VarListSpec
    
    AccListSpec
    
    PathListSpec
    
    MCPAccess
    
    Pretty
    
    A
    
    Queries
    
    VDQ
    
    ID
    
    LS
    
    TS
    
    ES
    
    VS
    
    NS
    
    NFL
    
    TC
    
    ThreadNodeLattice
    
    ML
    
    VI
    
    VarQuery
    
    FlatYojson
    
    SD
    
    VD
    
    AD
    
    MayBool
    
    MustBool
    
    Unit
    
    ProtectionKind
    
    Protection
    
    AllocationLocation
    
    YS
    
    Result
    
    Any
    
    Set
    
    Exceptionless
    
    Labels
    
    Hashtbl
    
    Exceptionless
    
    Infix
    
    Labels
    
    Events
    
    AnalysisResult
    
    ResultNode
    
    ResultConf
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    ResultType2
    
    ResultQuery
    
    Query
    
    NH
    
    SpecSysSol2
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    EQSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Make
    
    FileCfg
    
    Cfg
    
    SpecSys
    
    GobConfig
    
    AfterConfig
    
    AutoTune
    
    FunctionSet
    
    FunctionCallMap
    
    collectFunctionCallsVisitor
    
    functionVisitor
    
    findAllocsInLoops
    
    modVisitor
    
    modFunctionAnnotatorVisitor
    
    enumVisitor
    
    addTypeAttributeVisitor
    
    VariableMap
    
    VariableSet
    
    octagonVariableVisitor
    
    octagonFunctionVisitor
    
    AutoSoundConfig
    
    JsonSchema
    
    Options
    
    Base
    
    A
    
    H
    
    Q
    
    ID
    
    FD
    
    IdxDom
    
    AD
    
    Addr
    
    Offs
    
    ZeroInit
    
    LF
    
    CArrays
    
    PU
    
    VD
    
    CPA
    
    Dep
    
    WeakUpdates
    
    BaseComponents
    
    MainFunctor
    
    A
    
    Dom
    
    D
    
    C
    
    P
    
    V
    
    G
    
    VarH
    
    Exceptionless
    
    Infix
    
    Labels
    
    VarMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    InvariantEval
    
    D
    
    V
    
    G
    
    Invariant
    
    MainSpec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    RelationAnalysis
    
    ApronAnalysis
    
    AffineEqualityAnalysis
    
    LinearTwoVarEqualityAnalysis
    
    VarEq
    
    Addr
    
    Offs
    
    AD
    
    Exp
    
    LF
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    B
    
    E
    
    C
    
    CondVars
    
    Domain
    
    V
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    TmpSpecial
    
    VarEq
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    ML
    
    Deps
    
    MLDeps
    
    D
    
    C2poAnalysis
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    Region
    
    RegMap
    
    RegPart
    
    Reg
    
    Spec
    
    P
    
    D
    
    G
    
    C
    
    V
    
    Lvals
    
    A
    
    MallocFresh
    
    Spec
    
    G
    
    V
    
    P
    
    D
    
    C
    
    A
    
    Malloc_null
    
    AD
    
    IdxDom
    
    Offs
    
    Spec
    
    G
    
    V
    
    A
    
    Addr
    
    D
    
    C
    
    P
    
    MemLeak
    
    ToppedVarInfoSet
    
    WasMallocCalled
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    UseAfterFree
    
    AllocaVars
    
    HeapVars
    
    StackAndHeapVars
    
    ThreadIdToJoinedThreadsMap
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    MemOutOfBounds
    
    AS
    
    VDQ
    
    ID
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    MutexEventsAnalysis
    
    M
    
    Addr
    
    LF
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    LocksetAnalysis
    
    DS
    
    Make
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    MayArg
    
    D
    
    G
    
    V
    
    MakeMay
    
    P
    
    A
    
    D
    
    C
    
    G
    
    V
    
    MustArg
    
    D
    
    G
    
    V
    
    MakeMust
    
    P
    
    A
    
    D
    
    C
    
    G
    
    V
    
    MutexTypeAnalysis
    
    MAttr
    
    LF
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    MutexAnalysis
    
    M
    
    Mval
    
    Addr
    
    AddrRW
    
    MustLockset
    
    MustLocksetRW
    
    MustMultiplicity
    
    LF
    
    VarSet
    
    Spec
    
    Arg
    
    D
    
    V
    
    MakeP
    
    ReadWrite
    
    Write
    
    P
    
    GProtecting
    
    GProtected
    
    G
    
    C
    
    D
    
    P
    
    V
    
    GProtecting
    
    GProtected
    
    G
    
    GM
    
    A
    
    MayLocks
    
    LF
    
    Arg
    
    D
    
    G
    
    V
    
    Spec
    
    P
    
    A
    
    D
    
    C
    
    G
    
    V
    
    SymbLocks
    
    LF
    
    LP
    
    Exp
    
    ILock
    
    VarEq
    
    PS
    
    Spec
    
    G
    
    V
    
    P
    
    D
    
    C
    
    A
    
    PLock
    
    E
    
    Deadlock
    
    Spec
    
    LockEventPair
    
    MayLockEventPairs
    
    Arg
    
    D
    
    V
    
    Offs
    
    Mval
    
    G
    
    P
    
    A
    
    D
    
    C
    
    V
    
    G
    
    MutexGhosts
    
    NodeSet
    
    Spec
    
    P
    
    A
    
    D
    
    C
    
    V
    
    Locked
    
    Addr
    
    Unlocked
    
    Addr
    
    MultiThread
    
    G
    
    VariableSet
    
    ThreadFlag
    
    LF
    
    Spec
    
    Flag
    
    D
    
    C
    
    P
    
    V
    
    G
    
    A
    
    ThreadId
    
    LF
    
    Thread
    
    ThreadLifted
    
    VNI
    
    Spec
    
    G
    
    V
    
    N
    
    TD
    
    Created
    
    Current
    
    Callees
    
    D
    
    C
    
    P
    
    A
    
    ThreadAnalysis
    
    T
    
    TS
    
    Spec
    
    A
    
    D
    
    C
    
    G
    
    V
    
    D
    
    P
    
    ThreadJoins
    
    TID
    
    TIDs
    
    MustTIDs
    
    CleanExit
    
    Spec
    
    P
    
    A
    
    D
    
    C
    
    G
    
    V
    
    D
    
    MHPAnalysis
    
    Spec
    
    G
    
    V
    
    P
    
    D
    
    C
    
    A
    
    TID
    
    Pretty
    
    ThreadReturn
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    RaceAnalysis
    
    Spec
    
    P
    
    A
    
    D
    
    C
    
    V
    
    MemoSet
    
    OneOffset
    
    OffsetTrie
    
    Trie
    
    ChildMap
    
    G
    
    BasePriv
    
    VarQuery
    
    S
    
    D
    
    G
    
    V
    
    RelationPriv
    
    ThreadEscape
    
    M
    
    AD
    
    Spec
    
    P
    
    A
    
    ThreadIdSet
    
    D
    
    C
    
    V
    
    G
    
    PthreadSignals
    
    LF
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    PthreadBarriers
    
    LF
    
    Spec
    
    Barriers
    
    MustBarriers
    
    Capacity
    
    P
    
    V
    
    TID
    
    MCPAPlusTID
    
    Waiters
    
    Multiprocess
    
    G
    
    MustObserved
    
    D
    
    C
    
    A
    
    ExtractPthread
    
    uniqueVarPrinterClass
    
    Resource
    
    Action
    
    Tbls
    
    SymTblGen
    
    TblGen
    
    SymTbl
    
    Tbl
    
    ThreadTidTbl
    
    FunNameToTids
    
    MutexMidTbl
    
    CondVarIdTbl
    
    CtxTbl
    
    FunCallTbl
    
    NodeTbl
    
    Tasks
    
    Env
    
    Edges
    
    Variable
    
    Variables
    
    Codegen
    
    PmlResTbl
    
    FunTbl
    
    AdjacencyMatrix
    
    HashtblN
    
    Exceptionless
    
    Infix
    
    Labels
    
    Action
    
    Writer
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    PthreadOnce
    
    LF
    
    Mval
    
    Spec
    
    Onces
    
    ActiveOnces
    
    SeenOnces
    
    G
    
    V
    
    P
    
    D
    
    C
    
    A
    
    ActiveSetjmp
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    P
    
    ModifiedSinceSetjmp
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    D
    
    VS
    
    ActiveLongjmp
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    D
    
    PoisonVariables
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    VS
    
    D
    
    Vla
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    D
    
    Constants
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    Signs
    
    Signs
    
    SL
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    Taint
    
    VarinfoSet
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    UnitAnalysis
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    Assert
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    LoopTermination
    
    Statements
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    Callstring
    
    CallstringType
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    Callstring
    
    Callsite
    
    LoopfreeCallstring
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    Uninit
    
    M
    
    AD
    
    IdxDom
    
    Offs
    
    Spec
    
    G
    
    V
    
    A
    
    Addr
    
    D
    
    C
    
    P
    
    Expsplit
    
    M
    
    ID
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    BranchSet
    
    Spec
    
    G
    
    V
    
    A
    
    Branch
    
    BranchSet
    
    D
    
    C
    
    P
    
    StackTrace
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    SpecLoc
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    Spec1
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    Spec2
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    AccessAnalysis
    
    LF
    
    Spec
    
    P
    
    A
    
    D
    
    C
    
    V
    
    G
    
    WrapperFunctionAnalysis
    
    Q
    
    UniqueCountArgs
    
    MakeUniqueCount
    
    MallocUniqueCount
    
    ThreadCreateUniqueCount
    
    NodeFlatLattice
    
    WrapperArgs
    
    SpecBase
    
    G
    
    V
    
    P
    
    A
    
    NodeFlatLattice
    
    UniqueCount
    
    UniqueCallCounter
    
    D
    
    C
    
    MallocWrapper
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    ThreadCreateWrapper
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    TaintPartialContexts
    
    AD
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    D
    
    VS
    
    UnassumeAnalysis
    
    Cil
    
    NH
    
    FH
    
    EH
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    C
    
    D
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    ExpRelation
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    AbortUnless
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    PtranalAnalysis
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    StartStateAnalysis
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    SingleThreadedLifter
    
    SingleThreadedLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    SpecLifters
    
    NameLifter
    
    LatticeLifter
    
    DomainLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    GlobalDomainLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    HashconsLifter
    
    NameLifter
    
    HConsedArg
    
    D
    
    G
    
    C
    
    V
    
    P
    
    PrintableLifter
    
    ContextLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    HashconsContextLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    HashCachedContextLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    OptEqual
    
    D
    
    G
    
    C
    
    V
    
    P
    
    LevelSliceLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    WidenContextLifterSide
    
    DD
    
    M
    
    D
    
    G
    
    C
    
    V
    
    P
    
    DeadCodeLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    PathSensitive2
    
    D
    
    G
    
    C
    
    V
    
    P
    
    DeadBranchLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    LongjmpLifter
    
    Lifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    RecursionTermLifter
    
    Lifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    ContextGasLifter
    
    WideningDelay
    
    LocalChainParams
    
    GlobalChainParams
    
    Dom
    
    Chain
    
    DLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    GLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    WideningToken
    
    Uuid
    
    Index
    
    WideningTokenLifter
    
    Token
    
    TS
    
    Dom
    
    Lifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    Printable
    
    Lattice
    
    BoolDomain
    
    SetDomain
    
    MapDomain
    
    TrieDomain
    
    DisjointDomain
    
    HoareDomain
    
    PartitionDomain
    
    FlagHelper
    
    IntDomain
    
    FloatDomain
    
    Mval
    
    Offset
    
    StringDomain
    
    AddressDomain
    
    StructDomain
    
    UnionDomain
    
    ArrayDomain
    
    NullByteSet
    
    JmpBufDomain
    
    BaseDomain
    
    VD
    
    CPA
    
    M0
    
    M
    
    Group
    
    GroupMap
    
    PartDeps
    
    VarSet
    
    WeakUpdates
    
    BaseComponents
    
    ExpEvaluator
    
    DomFunctor
    
    DomWithTrivialExpEval
    
    ValueDomain
    
    ValueDomainQueries
    
    RelationDomain
    
    ApronDomain
    
    AffineEqualityDomain
    
    AffineEqualityDenseDomain
    
    LinearTwoVarEqualityDomain
    
    CongruenceClosure
    
    Tuple3
    
    Tuple2
    
    T
    
    TMap
    
    TSet
    
    UnionFind
    
    ZMap
    
    LookupMap
    
    M
    
    TUF
    
    LMap
    
    BlDis
    
    Disequalities
    
    SSet
    
    MRMap
    
    NormalFormEval
    
    LazyNormalFormEval
    
    MayBeEqual
    
    AD
    
    UnionFind
    
    M
    
    Tuple3
    
    Tuple2
    
    T
    
    TMap
    
    TSet
    
    UnionFind
    
    ValMap
    
    ZMap
    
    LookupMap
    
    C2poDomain
    
    M
    
    C2PODomain
    
    D
    
    MutexAttrDomain
    
    LockDomain
    
    IndexDomain
    
    Mval
    
    Addr
    
    MustLock
    
    MustLockset
    
    RW
    
    MakeRW
    
    MvalRW
    
    AddrRW
    
    MustLockRW
    
    MustLocksetRW
    
    MustMultiplicity
    
    Count
    
    MayLocksetNoRW
    
    Addr
    
    SymbLocksDomain
    
    M
    
    Exp
    
    LockingPattern
    
    ILock
    
    Idx
    
    Symbolic
    
    S
    
    DeadlockDomain
    
    Lock
    
    LockEvent
    
    MayLockEvents
    
    ThreadFlagDomain
    
    S
    
    Trivial
    
    Simple
    
    ThreadIdDomain
    
    ConcDomain
    
    MHP
    
    TID
    
    Pretty
    
    EscapeDomain
    
    EscapedVars
    
    PthreadDomain
    
    Tid
    
    Ctx
    
    Pred
    
    Base
    
    D
    
    Basetype
    
    Lval
    
    Access
    
    M
    
    TSH
    
    MemoRoot
    
    Memo
    
    A
    
    AS
    
    WarnAccs
    
    AccessDomain
    
    Event
    
    EventSet
    
    MusteqDomain
    
    V
    
    F
    
    F
    
    I
    
    VF
    
    P
    
    Equ
    
    RegionDomain
    
    B
    
    VFB
    
    RS
    
    RegPart
    
    S
    
    RegMap
    
    Reg
    
    RegionDom
    
    StackDomain
    
    S
    
    Dom1
    
    VarLat
    
    Var
    
    Dom2
    
    Var
    
    Loc
    
    Dom3
    
    DomainProperties
    
    DomainTest
    
    S
    
    Equal
    
    Leq
    
    Join
    
    Meet
    
    Bot
    
    Top
    
    Connect
    
    Widen
    
    Narrow
    
    All
    
    AllNonAssoc
    
    AbstractionDomainProperties
    
    AbstractFunction
    
    AbstractTest
    
    Monotone
    
    ValidTest
    
    IntDomainProperties
    
    OldS
    
    OldSWithIkind
    
    Ikind
    
    S
    
    WithIkind
    
    Ikind
    
    IntegerSet
    
    Base
    
    Valid
    
    All
    
    AllNonAssoc
    
    CompareCIL
    
    CompareAST
    
    CompareCFG
    
    UpdateCil
    
    MaxIdUtil
    
    Serialize
    
    CilMaps
    
    Messages
    
    Logs
    
    Preprocessor
    
    FpathH
    
    Exceptionless
    
    Infix
    
    Labels
    
    CompilationDatabase
    
    MakefileUtil
    
    TerminationPreprocessing
    
    VarToStmt
    
    loopCounterVisitor
    
    Witness
    
    M
    
    Result
    
    Query
    
    ArgTool
    
    Query
    
    CfgNode
    
    Node
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    NHT
    
    BiArgInvariant
    
    Node
    
    Edge
    
    Svcomp
    
    Specification
    
    Task
    
    Cfg
    
    Result
    
    SvcompSpec
    
    Invariant
    
    InvariantCil
    
    WitnessUtil
    
    NH
    
    NS
    
    Invariant
    
    YamlInvariant
    
    YamlInvariantValidate
    
    InvariantExp
    
    ES
    
    InvariantParser
    
    VarinfoH
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    YamlWitness
    
    Entry
    
    Make
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    WitnessInvariant
    
    FMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    FCMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    LH
    
    Exceptionless
    
    Infix
    
    Labels
    
    ValidationResult
    
    ChainParams
    
    Validator
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    LvarS
    
    WitnessInvariant
    
    InvariantParser
    
    VR
    
    YamlWitnessType
    
    Producer
    
    Task
    
    Metadata
    
    Location
    
    Invariant
    
    LoopInvariant
    
    LocationInvariant
    
    FlowInsensitiveInvariant
    
    PreconditionLoopInvariant
    
    InvariantSet
    
    LoopInvariant
    
    LocationInvariant
    
    InvariantType
    
    Invariant
    
    Target
    
    Certification
    
    LoopInvariantCertificate
    
    PreconditionLoopInvariantCertificate
    
    ViolationSequence
    
    Constraint
    
    Value
    
    Assumption
    
    Target
    
    FunctionEnter
    
    FunctionReturn
    
    Branching
    
    WaypointType
    
    Waypoint
    
    Segment
    
    GhostInstrumentation
    
    Initial
    
    Variable
    
    Update
    
    LocationUpdate
    
    EntryType
    
    Entry
    
    WitnessGhost
    
    Var
    
    Map
    
    Sarif
    
    SarifType
    
    Invocation
    
    Region
    
    ArtifactLocation
    
    PhysicalLocation
    
    Artifact
    
    Location
    
    Message
    
    ReportingDescriptor
    
    ToolComponent
    
    Tool
    
    Result
    
    Run
    
    SarifLog
    
    SarifRules
    
    MyARG
    
    Node
    
    Edge
    
    CFGEdge
    
    InlineEdgePrintable
    
    InlineEdge
    
    S
    
    Node
    
    Edge
    
    StackNode
    
    Stack
    
    Node
    
    Edge
    
    IsInteresting
    
    InterestingArg
    
    Node
    
    Edge
    
    SIntra
    
    SIntraOpt
    
    CfgIntra
    
    UnCilLogicIntra
    
    UnCilTernaryIntra
    
    Intra
    
    Node
    
    Edge
    
    ArgConstraints
    
    PathSensitive3
    
    D
    
    G
    
    C
    
    V
    
    P
    
    ArgTools
    
    M
    
    BiArg
    
    Node
    
    Edge
    
    Stack
    
    Node
    
    Edge
    
    NodeStyles
    
    EnumerateNode
    
    Dot
    
    Make
    
    Query
    
    CfgNode
    
    Node
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Violation
    
    ViolationArg
    
    Node
    
    Edge
    
    Feasibility
    
    Node
    
    UnknownFeasibility
    
    Node
    
    PathArg
    
    Node
    
    Edge
    
    ViolationZ3
    
    WP
    
    ObserverAutomaton
    
    S
    
    KMPArg
    
    KMP
    
    ObserverAnalysis
    
    StepObserverAutomaton
    
    MakeSpec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    PathArg
    
    MakePathSpec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    Refinement
    
    Transform
    
    M
    
    S
    
    PartialEval
    
    visitor
    
    DeadCode
    
    RemoveDeadCode
    
    EvalAssert
    
    EvalAssert
    
    visitor
    
    ExpressionEvaluation
    
    ExpEval
    
    Timing
    
    GoblintDir
    
    IntOps
    
    FloatOps
    
    LazyEval
    
    ResettableLazy
    
    ProcessPool
    
    Timeout
    
    Unix
    
    Js
    
    TimeUtil
    
    MessageUtil
    
    AnsiColors
    
    XmlUtil
    
    GobExn
    
    CilType
    
    Cilfacade
    
    CilLocation
    
    RichVarinfo
    
    DuplicateVars
    
    M
    
    VarType
    
    VarVarinfoMap
    
    Var
    
    CilCfg
    
    allBBVisitor
    
    countLoopsVisitor
    
    LoopUnrolling
    
    AccessKind
    
    LibraryDesc
    
    LibraryDsl
    
    LibraryFunctions
    
    BaseUtil
    
    PrecisionUtil
    
    ContextUtil
    
    ReturnUtil
    
    AD
    
    BaseInvariant
    
    M
    
    VD
    
    ID
    
    FD
    
    AD
    
    Eval
    
    D
    
    V
    
    G
    
    Make
    
    CommonPriv
    
    Q
    
    IdxDom
    
    VD
    
    AtomicParam
    
    NoAtomic
    
    ConfCheck
    
    RequireMutexActivatedInit
    
    RequireMutexPathSensOneMainInit
    
    RequireThreadFlagPathSensInit
    
    Protection
    
    MutexGlobals
    
    VMutex
    
    VMutexInits
    
    VGlobal
    
    V
    
    MayVars
    
    MustVars
    
    Locksets
    
    MustLockset
    
    MinLocksets
    
    WriteCenteredD
    
    W
    
    P
    
    Digest
    
    ThreadDigest
    
    ThreadNotStartedDigest
    
    PerMutexTidCommon
    
    TID
    
    W
    
    V
    
    LLock
    
    LMust
    
    L
    
    GMutex
    
    GThread
    
    G
    
    D
    
    PerMutexTidCommonNC
    
    TID
    
    W
    
    V
    
    LLock
    
    L
    
    GMutex
    
    GThread
    
    G
    
    D
    
    LMust
    
    WideningThresholds
    
    Vector
    
    Vector
    
    Matrix
    
    Matrix
    
    ArrayVector
    
    ArrayVector
    
    ArrayVectorFunctor
    
    ArrayVector
    
    ArrayMatrix
    
    ArrayMatrix
    
    ArrayMatrixFunctor
    
    ArrayMatrix
    
    SparseVector
    
    M
    
    SparseVector
    
    SparseVectorFunctor
    
    SparseVector
    
    ListMatrix
    
    M
    
    SparseMatrix
    
    SparseMatrixFunctor
    
    ListMatrix
    
    RatOps
    
    RatOps
    
    ConvenienceOps
    
    SharedFunctions
    
    GobApron
    
    PrecCompare
    
    Pretty
    
    Comparison
    
    Make
    
    MakeHashtbl
    
    CompareD
    
    MakeDump
    
    CompareDump
    
    CompareD
    
    PrecCompareUtil
    
    LocalizedPrintable
    
    R
    
    Key
    
    Dom
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
    
    S
    
    Key
    
    Dom
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Util
    
    Key
    
    Dom
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
    
    PrivPrecCompareUtil
    
    LV
    
    Util
    
    Key
    
    Dom
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Key
    
    Dom
    
    RH
    
    RelationPrecCompareUtil
    
    ApronPrecCompareUtil
    
    GobFormat
- Library goblint.library
  - AccessKind
  - LibraryDesc
    
    Cil
    
    Access
    
    Accesses
    
    MathPrintable
    
    MathLifted
  - LibraryDsl
  - LibraryFunctions
- Library goblint.logs
  - Goblint_logs
    
    AnsiColors
    
    Logs
    
    Level
    
    Result
    
    Kind
    
    PrettyKind
    
    FormatKind
    
    BatteriesKind
    
    MakeKind
    
    Pretty
    
    Format
    
    Batteries
- Library goblint.parallel
  - Goblint_parallel
    
    DomainsafeLazy
    
    GobMutex
    
    Threadpool
    
    Data
    
    DefaultType
    
    ConcurrentHashmap
- Library goblint.sites
  - Goblint_sites
- Library goblint.solver
  - Goblint_solver
    
    Td3
    
    M
    
    Hooks
    
    S
    
    Var
    
    Dom
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Base
    
    EqS0
    
    Var
    
    Dom
    
    VS
    
    Exceptionless
    
    Labels
    
    UpdateRule
    
    CurrentVarS
    
    S
    
    Var
    
    Dom
    
    S
    
    EqS
    
    Var
    
    Dom
    
    Basic
    
    DepVals
    
    Td_simplified
    
    M
    
    Base
    
    Td_simplified_ref
    
    M
    
    Base
    
    TopDown
    
    WP
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    TopDown_term
    
    WP
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    TopDown_space_cache_term
    
    WP
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    TopDown_deprecated
    
    TD3
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    SLRphased
    
    Make
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    SLRterm
    
    SLR3term
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    SLR
    
    SLR3
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Version
    
    Make0
    
    X
    
    XY
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    D
    
    Make
    
    X
    
    XY
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    D
    
    MyGenericEqSolver
    
    X
    
    PrintInfluence
    
    S1
    
    X
    
    TwoPhased
    
    N
    
    X
    
    XY
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    D
    
    W
    
    X
    
    XY
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    D
    
    JustWiden
    
    X
    
    XY
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    D
    
    EffectWConEq
    
    Make
    
    VS
    
    Exceptionless
    
    Labels
    
    Worklist
    
    Make
    
    VS
    
    Exceptionless
    
    Labels
    
    Generic
    
    LoadRunSolver
    
    LoadRunIncrSolver
    
    SolverStats
    
    DirtyBoxSolver
    
    SoundBoxSolverImpl
    
    SoundBoxSolver
    
    PreciseSideEffectBoxSolver
    
    Selector
    
    Make
    
    PostSolver
    
    Pretty
    
    M
    
    S
    
    S
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    F
    
    S
    
    VH
    
    Unit
    
    S
    
    VH
    
    Compose
    
    S
    
    VH
    
    Prune
    
    S
    
    VH
    
    Verify
    
    S
    
    VH
    
    Warn
    
    S
    
    VH
    
    SaveRun
    
    S
    
    VH
    
    StartEqConstrSys
    
    Var
    
    Dom
    
    EqConstrSysFromStartEqConstrSys
    
    Var
    
    Dom
    
    IncrS
    
    S
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    MakeIncr
    
    S
    
    VH
    
    MakeListArg
    
    S
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    M
    
    S
    
    VH
    
    MakeIncrListArg
    
    S
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    M
    
    S
    
    VH
    
    MakeIncrList
    
    S
    
    VH
    
    MakeList
    
    IncrArg
    
    S
    
    VH
    
    M
    
    S
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    MakeStdArg
    
    ListArgFromStdArg
    
    S
    
    VH
    
    M
    
    S
    
    VH
    
    EqIncrSolverFromEqSolver
    
    DemandEqIncrSolverFromEqSolver
    
    LocalFixpoint
    
    Make
    
    SolverStats
    
    SolverBox
    
    S
    
    Warrow
    
    Widen
    
    NarrowOption
    
    SideWPointSelect
    
    S
    
    Always
    
    Never
    
    SidesLocal
    
    SidesPP
    
    Sides
    
    UnstableSelf
    
    UnstableCalled
    
    Cycle
    
    Td3UpdateRule
    
    S
    
    Inactive
    
    Narrow
- Library goblint.std
  - Goblint_std
    
    GobArray
    
    GobGc
    
    GobHashtbl
    
    Pretty
    
    GobList
    
    Syntax
    
    GobRef
    
    GobResult
    
    Syntax
    
    GobOption
    
    Syntax
    
    GobSys
    
    GobUnix
    
    GobTuple
    
    Tuple6
    
    GobFpath
    
    GobPretty
    
    GobQCheck
    
    Gen
    
    Iter
    
    Shrink
    
    Arbitrary
    
    GobYaml
    
    GobYojson
    
    GobZ
- Library goblint.timing
  - Goblint_timing
    
    Name
    
    S
    
    Make
- Library goblint.tracing
  - Goblint_tracing
    
    Strs
- Library goblint_cdomain_value
  - AddressDomain
    
    AddressBase
    
    AddressPrintable
    
    AddressLattice
    
    AddressLatticeRepr
    
    VariableRepr
    
    UnitOffsetRepr
    
    AddressSet
    
    Addr
  - AddressDomain_intf
    
    AddressDomain
    
    AddressBase
    
    AddressPrintable
    
    AddressLattice
    
    AddressLatticeRepr
    
    VariableRepr
    
    UnitOffsetRepr
    
    AddressSet
    
    Addr
  - ArrayDomain
    
    VDQ
    
    S0
    
    S
    
    Str
    
    StrWithDomain
    
    LatticeWithInvalidate
    
    LatticeWithSmartOps
    
    Null
    
    LatticeWithNull
    
    Trivial
    
    TrivialWithLength
    
    Partitioned
    
    PartitionedWithLength
    
    NullByte
    
    AttributeConfiguredArrayDomain
    
    AttributeConfiguredAndNullByteArrayDomain
  - BitfieldDomain
    
    InfixIntOps
    
    BitfieldArith
    
    BitfieldFunctor
    
    Bitfield
  - ConcDomain
    
    ThreadSet
    
    MustThreadSet
    
    CreatedThreadSet
    
    ThreadCreation
    
    UNames
    
    Uniqueness
    
    ParentThreadSet
    
    DirtyExitNames
    
    DirtyExit
    
    ThreadStringSet
  - CongruenceDomain
    
    Congruence
  - DefExcDomain
    
    BISet
    
    Exclusion
    
    R
    
    DefExc
  - EnumsDomain
    
    Enums
  - FloatDomain
    
    FloatArith
    
    FloatDomainBase
    
    F64Interval
    
    F32Interval
    
    FloatDomain
    
    FloatDomTupleImpl
  - IntDomTuple
    
    IntDomTupleImpl
    
    I1
    
    I2
    
    I3
    
    I4
    
    I5
    
    I6
    
    IntDomTuple
    
    I
  - IntDomain
    
    Arith
    
    ArithIkind
    
    B
    
    IkindUnawareS
    
    S
    
    SOverflow
    
    SOverflowUnlifter
    
    Y
    
    Z
    
    IntDomLifter
    
    Ikind
    
    PtrDiffIkind
    
    IntDomWithDefaultIkind
    
    IntDomTuple
    
    Size
    
    BISet
    
    Integers
    
    FlatPureIntegers
    
    Flattened
    
    Lifted
    
    IntervalFunctor
    
    BitfieldFunctor
    
    IntervalSetFunctor
    
    Interval32
    
    Interval
    
    Bitfield
    
    IntervalSet
    
    Congruence
    
    DefExc
    
    Flat
    
    Lift
    
    Enums
  - IntDomain0
    
    Arith
    
    ArithIkind
    
    B
    
    IkindUnawareS
    
    S
    
    SOverflow
    
    Y
    
    Z
    
    Ikind
    
    IntDomain
    
    M
    
    Bitfield_SOverflow
    
    IntDomLifter
    
    PtrDiffIkind
    
    IntDomWithDefaultIkind
    
    Size
    
    StdTop
    
    Std
    
    IntervalArith
    
    IntInvariant
    
    SOverflowUnlifter
    
    IntIkind
    
    Integers
    
    FlatPureIntegers
    
    Flat
    
    Lift
    
    Flattened
    
    Lifted
    
    SOverflowLifter
  - IntDomain_intf
    
    Arith
    
    ArithIkind
    
    B
    
    IkindUnawareS
    
    S
    
    SOverflow
    
    Y
    
    Z
    
    Ikind
    
    IntDomain
    
    Arith
    
    ArithIkind
    
    B
    
    IkindUnawareS
    
    S
    
    SOverflow
    
    SOverflowUnlifter
    
    Y
    
    Z
    
    IntDomLifter
    
    Ikind
    
    PtrDiffIkind
    
    IntDomWithDefaultIkind
    
    IntDomTuple
    
    Size
    
    BISet
    
    Integers
    
    FlatPureIntegers
    
    Flattened
    
    Lifted
    
    IntervalFunctor
    
    BitfieldFunctor
    
    IntervalSetFunctor
    
    Interval32
    
    Interval
    
    Bitfield
    
    IntervalSet
    
    Congruence
    
    DefExc
    
    Flat
    
    Lift
    
    Enums
  - IntervalDomain
    
    IntervalFunctor
    
    Interval
    
    Interval32
  - IntervalSetDomain
    
    IntervalSetFunctor
    
    IntervalSet
  - Invariant
    
    ExpLat
    
    N
  - InvariantCil
    
    exp_replace_original_name_visitor
    
    exp_deep_unroll_types_visitor
    
    exp_is_in_scope_visitor
    
    exp_contains_tmp_visitor
    
    exp_contains_anon_type_visitor
  - JmpBufDomain
    
    BufferEntry
    
    BufferEntryOrTop
    
    JmpBufSet
    
    JmpBufSetTaint
    
    Bufs
    
    NodeSet
    
    ActiveLongjmps
    
    LocallyModifiedMap
    
    VarSet
  - Lval
    
    Set
  - MutexAttrDomain
    
    MutexKind
  - Mval
    
    Printable
    
    Lattice
    
    MakePrintable
    
    MakeLattice
    
    Unit
    
    Exp
    
    Z
  - Mval_intf
    
    Printable
    
    Lattice
    
    Mval
    
    Printable
    
    Lattice
    
    MakePrintable
    
    MakeLattice
    
    Unit
    
    Exp
    
    Z
  - NullByteSet
    
    MustSet
    
    M
    
    MaySet
    
    M
    
    MustMaySet
    
    Set
  - Offset
    
    Index
    
    Printable
    
    Lattice
    
    Unit
    
    Exp
    
    Z
    
    Poly
    
    Printable
    
    Lattice
    
    MakePrintable
    
    MakeLattice
    
    Unit
    
    Exp
    
    Z
  - Offset_intf
    
    Index
    
    Printable
    
    Lattice
    
    Printable
    
    Lattice
    
    Offset
    
    Index
    
    Printable
    
    Lattice
    
    Unit
    
    Exp
    
    Z
    
    Poly
    
    Printable
    
    Lattice
    
    MakePrintable
    
    MakeLattice
    
    Unit
    
    Exp
    
    Z
  - PreValueDomain
    
    ID
    
    FD
    
    IndexDomain
    
    Offs
    
    Mval
    
    AD
    
    Addr
    
    Addr
    
    Offs
    
    Mval
  - PrecisionUtil
  - StringDomain
  - StructDomain
    
    Arg
    
    S
    
    Simple
    
    Sets
    
    KeyedSets
    
    FlagConfiguredStructDomain
  - ThreadIdDomain
    
    S
    
    Stateless
    
    Stateful
    
    D
    
    FunNode
    
    Unit
    
    D
    
    History
    
    D
    
    ThreadLiftNames
    
    Lift
    
    FlagConfiguredTID
    
    D
    
    Thread
    
    D
    
    ThreadLifted
  - UnionDomain
    
    Arg
    
    S
    
    Field
    
    Simple
  - ValueDomain
    
    ID
    
    FD
    
    IndexDomain
    
    Mval
    
    Addr
    
    Offs
    
    M
    
    MutexAttr
    
    VDQ
    
    AD
    
    AddrSetDomain
    
    ArrIdxDomain
    
    S
    
    Blob
    
    ZeroInit
    
    ZeroInit
    
    Blob
    
    Threads
    
    JmpBufs
    
    Compound
    
    Structs
    
    Unions
    
    CArrays
    
    Blobs
    
    InvariantArg
    
    ValueInvariant
    
    VS
  - ValueDomainQueries
    
    LS
    
    AD
    
    ID
    
    I
  - WideningThresholds
    
    Thresholds
  - WrapperFunctionAnalysis0
    
    UniqueCountArgs
    
    MakeUniqueCount
    
    MallocUniqueCount
    
    ThreadCreateUniqueCount
    
    NodeFlatLattice
- Sources
  - goblint.backtrace
    
    goblint_backtrace.ml
  - goblint.build-info
    
    configDatetime.ml
    
    configOcaml.ml
    
    configProfile.ml
    
    configVersion.ml
    
    dune_build_info.ml
    
    goblint_build_info.ml
    
    goblint_build_info__.ml
  - goblint.config
    
    afterConfig.ml
    
    gobConfig.ml
    
    jsonSchema.ml
    
    options.ml
  - goblint.constraint
    
    constrSys.ml
    
    goblint_constraint.ml
    
    goblint_constraint__.ml
    
    solverTypes.ml
    
    translators.ml
    
    varQuery.ml
  - goblint.domain
    
    boolDomain.ml
    
    disjointDomain.ml
    
    flagHelper.ml
    
    hoareDomain.ml
    
    lattice.ml
    
    mapDomain.ml
    
    partitionDomain.ml
    
    setDomain.ml
    
    trieDomain.ml
  - goblint.incremental
    
    cilMaps.ml
    
    compareAST.ml
    
    compareCFG.ml
    
    compareCIL.ml
    
    makefileUtil.ml
    
    maxIdUtil.ml
    
    serialize.ml
    
    updateCil.ml
  - goblint.lib
    
    affineEqualityAnalysis.ml
    
    affineEqualityDenseDomain.ml
    
    affineEqualityDomain.ml
    
    apronAnalysis.ml
    
    apronDomain.ml
    
    apronPrecCompareUtil.ml
    
    autoTune.ml
    
    autoTune0.ml
    
    gobApron.ml
    
    goblint_lib.ml
    
    goblint_lib__.ml
    
    linearTwoVarEqualityAnalysis.ml
    
    linearTwoVarEqualityDomain.ml
    
    maingoblint.ml
    
    relationAnalysis.ml
    
    relationDomain.ml
    
    relationPrecCompareUtil.ml
    
    relationPriv.ml
    
    sharedFunctions.ml
    
    violationZ3.ml
  - goblint.library
    
    accessKind.ml
    
    libraryDesc.ml
    
    libraryDsl.ml
    
    libraryFunctions.ml
  - goblint.logs
    
    ansiColors.ml
    
    goblint_logs.ml
    
    logs.ml
  - goblint.parallel
    
    data.ml
    
    domainsafeLazy.ml
    
    gobMutex.ml
    
    goblint_parallel.ml
    
    goblint_parallel__.ml
    
    threadpool.ml
  - goblint.sites
    
    Dunesite.ml
    
    goblint_sites.ml
    
    goblint_sites__.ml
  - goblint.solver
    
    effectWConEq.ml
    
    generic.ml
    
    goblint_solver.ml
    
    goblint_solver__.ml
    
    localFixpoint.ml
    
    postSolver.ml
    
    sLR.ml
    
    sLRphased.ml
    
    sLRterm.ml
    
    selector.ml
    
    sideWPointSelect.ml
    
    solverBox.ml
    
    solverStats.ml
    
    td3.ml
    
    td3UpdateRule.ml
    
    td_simplified.ml
    
    td_simplified_ref.ml
    
    topDown.ml
    
    topDown_deprecated.ml
    
    topDown_space_cache_term.ml
    
    topDown_term.ml
    
    worklist.ml
  - goblint.std
    
    gobArray.ml
    
    gobFpath.ml
    
    gobGc.ml
    
    gobHashtbl.ml
    
    gobList.ml
    
    gobOption.ml
    
    gobPretty.ml
    
    gobQCheck.ml
    
    gobRef.ml
    
    gobResult.ml
    
    gobSys.ml
    
    gobTuple.ml
    
    gobUnix.ml
    
    gobYaml.ml
    
    gobYojson.ml
    
    gobZ.ml
    
    goblint_std.ml
    
    goblint_std__.ml
  - goblint.timing
    
    goblint_timing.ml
    
    goblint_timing__.ml
    
    goblint_timing_intf.ml
  - goblint.tracing
    
    goblint_tracing.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Goblint_lib.StartStateAnalysis`

Remembers the abstract address value of each parameter at the beginning of each function by adding a ghost variable for each parameter. Used by the c2po analysis.

module Spec : Analyses.MCPSpec

First, all parameters (=formals) of the function are duplicated (by using DuplicateVars), then, we remember the value of each local variable at the beginning of the function a new duplicated variable.

package goblint

Module Goblint_lib.StartStateAnalysis

Module `Goblint_lib.StartStateAnalysis`