package goblint

You can search for identifiers within the package.

in-package search v0.2.0

package goblint

goblint
- CHANGELOG
- README
- Library goblint.backtrace
  - Goblint_backtrace
- Library goblint.build-info
  - Goblint_build_info
- Library goblint.lib
  - Goblint_lib
    
    Maingoblint
    
    Control
    
    S2S
    
    D
    
    G
    
    C
    
    V
    
    P
    
    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
    
    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
    
    CfgBackward
    
    CfgForward
    
    CfgBidir
    
    NodeH
    
    Exceptionless
    
    Infix
    
    Labels
    
    FileCfg
    
    Cfg
    
    CfgTools
    
    H
    
    NH
    
    SCC
    
    CfgEdge
    
    CfgEdgeH
    
    Exceptionless
    
    Infix
    
    Labels
    
    CfgPrinters
    
    NodeStyles
    
    CfgPrinters
    
    Analyses
    
    M
    
    SysVar
    
    VarType
    
    Var
    
    VarF
    
    SpecSysVar
    
    GVarF
    
    GVarG
    
    CSet
    
    Dom
    
    ResultNode
    
    ResultConf
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    MCPA
    
    MCPSpec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    MonSystem
    
    Var
    
    Dom
    
    EqConstrSys
    
    Var
    
    Dom
    
    GlobConstrSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    GenericEqIncrSolverBase
    
    IncrSolverArg
    
    GenericEqIncrSolver
    
    GenericEqSolver
    
    GenericGlobSolver
    
    ResultType2
    
    StdV
    
    VarinfoV
    
    EmptyV
    
    UnitA
    
    UnitP
    
    IdentityP
    
    DefaultSpec
    
    G
    
    V
    
    P
    
    A
    
    IdentitySpec
    
    G
    
    V
    
    P
    
    A
    
    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
    
    M
    
    HashconsLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    HashconsContextLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    OptEqual
    
    D
    
    G
    
    C
    
    V
    
    P
    
    LevelSliceLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    LimitLifter
    
    G
    
    C
    
    V
    
    P
    
    H
    
    D
    
    WidenContextLifterSide
    
    DD
    
    M
    
    D
    
    G
    
    C
    
    V
    
    P
    
    DeadCodeLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    Increment
    
    Var2
    
    FromSpec
    
    LVar
    
    GVar
    
    D
    
    G
    
    EqIncrSolverFromEqSolver
    
    EqConstrSysFromGlobConstrSys
    
    Var
    
    Dom
    
    GlobConstrSolFromEqConstrSolBase
    
    GlobConstrSolFromEqConstrSol
    
    S2
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    GlobSolverFromEqSolver
    
    EqSys
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Sol'
    
    Splitter
    
    PathSensitive2
    
    D
    
    G
    
    C
    
    V
    
    P
    
    DeadBranchLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    LongjmpLifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    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
    
    CurrentVarEqConstrSys
    
    S
    
    Var
    
    Dom
    
    AnalysisState
    
    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
    
    NFL
    
    TC
    
    ThreadNodeLattice
    
    ML
    
    VI
    
    FlatYojson
    
    SD
    
    VD
    
    MayBool
    
    MustBool
    
    Unit
    
    Protection
    
    Result
    
    Any
    
    Set
    
    Exceptionless
    
    Labels
    
    Hashtbl
    
    Exceptionless
    
    Infix
    
    Labels
    
    Events
    
    ResultQuery
    
    Query
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    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
    
    VarQuery
    
    GobConfig
    
    Validator
    
    ValidatorRequireAll
    
    S
    
    Impl
    
    AfterConfig
    
    AutoTune
    
    FunctionSet
    
    FunctionCallMap
    
    collectFunctionCallsVisitor
    
    functionVisitor
    
    modVisitor
    
    modFunctionAnnotatorVisitor
    
    enumVisitor
    
    addTypeAttributeVisitor
    
    VariableMap
    
    VariableSet
    
    octagonVariableVisitor
    
    octagonFunctionVisitor
    
    JsonSchema
    
    JS
    
    JE
    
    JQ
    
    Schema
    
    Validator
    
    Options
    
    Base
    
    A
    
    H
    
    Q
    
    ID
    
    FD
    
    IdxDom
    
    AD
    
    Addr
    
    Offs
    
    LF
    
    CArrays
    
    BI
    
    PU
    
    VD
    
    CPA
    
    Dep
    
    WeakUpdates
    
    BaseComponents
    
    MainFunctor
    
    P
    
    A
    
    Dom
    
    D
    
    C
    
    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
    
    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
    
    ML
    
    Deps
    
    MLDeps
    
    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
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    UseAfterFree
    
    ToppedVarInfoSet
    
    ThreadIdSet
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    MutexEventsAnalysis
    
    M
    
    Addr
    
    Lockset
    
    Mutexes
    
    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
    
    Addr
    
    Lockset
    
    Mutexes
    
    LF
    
    VarSet
    
    Spec
    
    Arg
    
    Multiplicity
    
    Count
    
    D
    
    V
    
    MakeP
    
    ReadWrite
    
    Write
    
    P
    
    GProtecting
    
    GProtected
    
    G
    
    C
    
    D
    
    P
    
    V
    
    GProtecting
    
    GProtected
    
    G
    
    GM
    
    Exceptionless
    
    Infix
    
    Labels
    
    A
    
    RW
    
    Lock
    
    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
    
    E
    
    Deadlock
    
    Spec
    
    LockEventPair
    
    MayLockEventPairs
    
    Arg
    
    D
    
    V
    
    Offs
    
    Mval
    
    G
    
    P
    
    A
    
    D
    
    C
    
    V
    
    G
    
    ThreadFlag
    
    LF
    
    Spec
    
    G
    
    V
    
    Flag
    
    D
    
    C
    
    P
    
    A
    
    ThreadId
    
    LF
    
    Thread
    
    ThreadLifted
    
    VNI
    
    Spec
    
    G
    
    V
    
    N
    
    TD
    
    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
    
    S
    
    D
    
    G
    
    V
    
    RelationPriv
    
    ThreadEscape
    
    M
    
    Spec
    
    P
    
    A
    
    ThreadIdSet
    
    D
    
    C
    
    V
    
    G
    
    PthreadSignals
    
    LF
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    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
    
    ActiveSetjmp
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    P
    
    ModifiedSinceLongjmp
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    VS
    
    C
    
    ActiveLongjmp
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    PoisonVariables
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    VS
    
    D
    
    C
    
    Vla
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    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
    
    FileUse
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    Uninit
    
    M
    
    AD
    
    IdxDom
    
    Offs
    
    Spec
    
    G
    
    V
    
    A
    
    Addr
    
    D
    
    C
    
    P
    
    Termination
    
    M
    
    TermDomain
    
    loopCounterVisitor
    
    loopBreaksVisitor
    
    loopVarsVisitor
    
    loopInstrVisitor
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    recomputeVisitor
    
    Expsplit
    
    M
    
    ID
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    StackTrace
    
    LF
    
    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
    
    Spec
    
    SC
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    SpecCheck
    
    AccessAnalysis
    
    LF
    
    Spec
    
    P
    
    A
    
    D
    
    C
    
    V
    
    G
    
    WrapperFunctionAnalysis
    
    Q
    
    UniqueCountArgs
    
    MakeUniqueCount
    
    MallocUniqueCount
    
    ThreadCreateUniqueCount
    
    NodeFlatLattice
    
    WrapperArgs
    
    SpecBase
    
    G
    
    V
    
    P
    
    A
    
    UniqueCount
    
    UniqueCallCounter
    
    D
    
    C
    
    MallocWrapper
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    ThreadCreateWrapper
    
    D
    
    G
    
    C
    
    V
    
    P
    
    A
    
    TaintPartialContexts
    
    Spec
    
    G
    
    V
    
    P
    
    A
    
    D
    
    C
    
    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
    
    Printable
    
    Pretty
    
    S
    
    Empty
    
    Std
    
    StdLeaf
    
    Showable
    
    SimpleShow
    
    Prettyable
    
    SimplePretty
    
    Name
    
    UnitConf
    
    Unit
    
    LiftingNames
    
    DefaultNames
    
    HConsed
    
    HC
    
    HashCached
    
    LazyHash
    
    Lift
    
    Either
    
    Option
    
    Lift2
    
    ProdConfiguration
    
    ProdConf
    
    Prod
    
    ProdSimple
    
    Prod3
    
    Prod4
    
    Liszt
    
    ChainParams
    
    Chain
    
    LiftBot
    
    LiftTop
    
    Strings
    
    FailwithMessage
    
    Failwith
    
    Yojson
    
    Lattice
    
    Pretty
    
    PO
    
    S
    
    UnitConf
    
    Unit
    
    NoBotTop
    
    Fake
    
    PD
    
    FakeSingleton
    
    Reverse
    
    HConsed
    
    HC
    
    HashCached
    
    LazyHash
    
    Flat
    
    Lift
    
    LiftPO
    
    Lift2
    
    ProdConf
    
    Prod
    
    ProdSimple
    
    Prod3
    
    Prod4
    
    LiftBot
    
    LiftTop
    
    Liszt
    
    Num
    
    ProdList
    
    Chain
    
    BoolDomain
    
    Bool
    
    MayBool
    
    MustBool
    
    SetDomain
    
    Pretty
    
    S
    
    Elements
    
    Print
    
    Make
    
    SensitiveConf
    
    Elt
    
    ToppedSetNames
    
    LiftTop
    
    ToppedSet
    
    HeadlessSet
    
    Reverse
    
    FiniteSetElems
    
    FiniteSet
    
    E
    
    Joined
    
    MapDomain
    
    Pretty
    
    PS
    
    S
    
    Bindings
    
    Print
    
    Groupable
    
    PrintGroupable
    
    Group
    
    GroupMap
    
    PMap
    
    HashCached
    
    HConsed
    
    Timed
    
    MapBot
    
    MapTop
    
    LiftTop
    
    MapBot_LiftTop
    
    LiftBot
    
    MapTop_LiftBot
    
    Joined
    
    TrieDomain
    
    Make
    
    Trie
    
    ChildMap
    
    DisjointDomain
    
    Representative
    
    ProjectiveSet
    
    MayEqualSetDomain
    
    ProjectiveSetPairwiseMeet
    
    Congruence
    
    PairwiseSet
    
    RepresentativeCongruence
    
    CombinedSet
    
    ProjectiveMap
    
    PairwiseMap
    
    HoareDomain
    
    Pretty
    
    HoarePO
    
    Map
    
    B
    
    SetS
    
    Set
    
    Set_LiftTop
    
    MapBot
    
    SetEM
    
    PartitionDomain
    
    Collapse
    
    Set
    
    CollapseSet
    
    Make
    
    S
    
    SetSet
    
    B
    
    E
    
    ExpPartitions
    
    B
    
    E
    
    FlagHelper
    
    FlagError
    
    FlagHelper
    
    LatticeFlagHelperArg
    
    LatticeFlagHelper
    
    IntDomain
    
    Arith
    
    ArithIkind
    
    B
    
    IkindUnawareS
    
    S
    
    SOverflow
    
    SOverflowUnlifter
    
    OldDomainFacade
    
    Y
    
    Z
    
    IntDomLifter
    
    Ikind
    
    PtrDiffIkind
    
    IntDomWithDefaultIkind
    
    IntDomTuple
    
    Size
    
    BISet
    
    Integers
    
    FlatPureIntegers
    
    Flattened
    
    FlattenedBI
    
    Lifted
    
    IntervalFunctor
    
    IntervalSetFunctor
    
    Interval32
    
    BigInt
    
    Interval
    
    IntervalSet
    
    Congruence
    
    DefExc
    
    Flat
    
    Lift
    
    Reverse
    
    Enums
    
    BooleansNames
    
    MakeBooleans
    
    Booleans
    
    FloatDomain
    
    FloatArith
    
    FloatDomainBase
    
    F64Interval
    
    F32Interval
    
    FloatDomain
    
    FloatDomTupleImpl
    
    Mval
    
    Printable
    
    Lattice
    
    MakePrintable
    
    MakeLattice
    
    Unit
    
    Exp
    
    Offset
    
    Index
    
    Printable
    
    Lattice
    
    Unit
    
    Exp
    
    Printable
    
    Lattice
    
    MakePrintable
    
    MakeLattice
    
    Unit
    
    Exp
    
    AddressDomain
    
    AddressBase
    
    AddressPrintable
    
    AddressLattice
    
    AddressLatticeRepr
    
    VariableRepr
    
    UnitOffsetRepr
    
    AddressSet
    
    Addr
    
    StructDomain
    
    Arg
    
    S
    
    Simple
    
    Sets
    
    KeyedSets
    
    FlagConfiguredStructDomain
    
    UnionDomain
    
    Arg
    
    S
    
    Field
    
    Simple
    
    ArrayDomain
    
    VDQ
    
    S
    
    LatticeWithSmartOps
    
    Trivial
    
    TrivialWithLength
    
    Partitioned
    
    PartitionedWithLength
    
    AttributeConfiguredArrayDomain
    
    JmpBufDomain
    
    BufferEntry
    
    BufferEntryOrTop
    
    JmpBufSet
    
    JmpBufSetTaint
    
    Bufs
    
    NodeSet
    
    ActiveLongjmps
    
    LocallyModifiedMap
    
    VarSet
    
    BaseDomain
    
    VD
    
    BI
    
    CPA
    
    M0
    
    M
    
    Group
    
    GroupMap
    
    PartDeps
    
    VarSet
    
    WeakUpdates
    
    BaseComponents
    
    ExpEvaluator
    
    DomFunctor
    
    DomWithTrivialExpEval
    
    ValueDomain
    
    ID
    
    FD
    
    IndexDomain
    
    Mval
    
    AD
    
    Addr
    
    Addr
    
    Offs
    
    Mval
    
    Offs
    
    M
    
    BI
    
    MutexAttr
    
    VDQ
    
    LS
    
    AddrSetDomain
    
    ArrIdxDomain
    
    S
    
    Blob
    
    ZeroInit
    
    Blob
    
    Threads
    
    JmpBufs
    
    Compound
    
    Structs
    
    Unions
    
    CArrays
    
    Blobs
    
    InvariantArg
    
    ValueInvariant
    
    VS
    
    ValueDomainQueries
    
    LS
    
    ID
    
    I
    
    RelationDomain
    
    ApronDomain
    
    AffineEqualityDomain
    
    MutexAttrDomain
    
    MutexKind
    
    LockDomain
    
    Addr
    
    Offs
    
    Exp
    
    IdxDom
    
    Mutexes
    
    Simple
    
    Priorities
    
    Lockset
    
    RW
    
    Lock
    
    MayLockset
    
    RW
    
    Lock
    
    MayLocksetNoRW
    
    Addr
    
    Symbolic
    
    S
    
    SymbLocksDomain
    
    M
    
    Exp
    
    LockingPattern
    
    ILock
    
    Idx
    
    DeadlockDomain
    
    Lock
    
    LockEvent
    
    MayLockEvents
    
    ThreadFlagDomain
    
    S
    
    Trivial
    
    Simple
    
    ThreadIdDomain
    
    S
    
    Stateless
    
    Stateful
    
    D
    
    FunNode
    
    Unit
    
    D
    
    History
    
    D
    
    ThreadLiftNames
    
    Lift
    
    FlagConfiguredTID
    
    D
    
    Thread
    
    ThreadLifted
    
    ConcDomain
    
    ThreadSet
    
    MustThreadSet
    
    CreatedThreadSet
    
    ThreadCreation
    
    UNames
    
    Uniqueness
    
    ParentThreadSet
    
    DirtyExitNames
    
    DirtyExit
    
    ThreadStringSet
    
    MHP
    
    TID
    
    Pretty
    
    EscapeDomain
    
    EscapedVars
    
    PthreadDomain
    
    Tid
    
    Ctx
    
    Pred
    
    Base
    
    D
    
    Basetype
    
    Variables
    
    RawStrings
    
    Strings
    
    RawBools
    
    Bools
    
    CilExp
    
    CilStmt
    
    CilField
    
    Lval
    
    Set
    
    Access
    
    M
    
    TSH
    
    Exceptionless
    
    Infix
    
    Labels
    
    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
    
    FileDomain
    
    D
    
    Val
    
    Dom
    
    K
    
    V
    
    MD
    
    StackDomain
    
    S
    
    Dom1
    
    VarLat
    
    Var
    
    Dom2
    
    Var
    
    Loc
    
    Dom3
    
    MvalMapDomain
    
    M
    
    S
    
    Value
    
    Domain
    
    K
    
    V
    
    MD
    
    SpecDomain
    
    D
    
    Val
    
    Dom
    
    K
    
    V
    
    MD
    
    DomainProperties
    
    DomainTest
    
    S
    
    Equal
    
    Leq
    
    Join
    
    Meet
    
    Bot
    
    Top
    
    Connect
    
    Widen
    
    Narrow
    
    All
    
    AllNonAssoc
    
    AbstractionDomainProperties
    
    AbstractFunction
    
    AbstractTest
    
    Monotone
    
    ValidTest
    
    IntDomainProperties
    
    BI
    
    OldS
    
    OldSWithIkind
    
    Ikind
    
    S
    
    WithIkind
    
    Ikind
    
    IntegerSet
    
    Base
    
    Valid
    
    All
    
    AllNonAssoc
    
    CompareCIL
    
    StringMap
    
    NH
    
    FundecForMap
    
    FundecMap
    
    VarinfoOrdered
    
    VarinfoMap
    
    GlobalMap
    
    GlobalColMap
    
    VarinfoSet
    
    CompareAST
    
    StringMap
    
    CompareCFG
    
    StringMap
    
    NH
    
    UpdateCil
    
    NodeMap
    
    MaxIdUtil
    
    Serialize
    
    Cache
    
    CilMaps
    
    FundecForMap
    
    FundecMap
    
    VarinfoOrdered
    
    VarinfoMap
    
    Td3
    
    Hooks
    
    S
    
    Var
    
    Dom
    
    HM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Base
    
    VS
    
    Exceptionless
    
    Labels
    
    CurrentVarS
    
    S
    
    Var
    
    Dom
    
    S
    
    Basic
    
    DepVals
    
    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
    
    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
    
    LocalFixpoint
    
    Make
    
    SolverStats
    
    SolverBox
    
    S
    
    Warrow
    
    Widen
    
    NarrowOption
    
    Messages
    
    Pretty
    
    Category
    
    Behavior
    
    Undefined
    
    ArrayOutOfBounds
    
    Integer
    
    Cast
    
    Severity
    
    Location
    
    Piece
    
    MultiPiece
    
    Tag
    
    Tags
    
    Message
    
    Table
    
    MH
    
    Strs
    
    Tracing
    
    Strs
    
    Preprocessor
    
    FpathH
    
    Exceptionless
    
    Infix
    
    Labels
    
    CompilationDatabase
    
    MakefileUtil
    
    Svcomp
    
    Specification
    
    Task
    
    Cfg
    
    Result
    
    TaskResult
    
    Arg
    
    Node
    
    Edge
    
    StackTaskResult
    
    Arg
    
    Node
    
    Edge
    
    SvcompSpec
    
    Invariant
    
    ExpLat
    
    N
    
    InvariantCil
    
    exp_replace_original_name_visitor
    
    exp_is_in_scope_visitor
    
    exp_contains_tmp_visitor
    
    WitnessUtil
    
    NH
    
    NS
    
    Invariant
    
    InvariantExp
    
    ES
    
    InvariantParser
    
    VarinfoH
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    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
    
    WitnessConstraints
    
    PathSensitive3
    
    D
    
    G
    
    C
    
    V
    
    P
    
    ArgTools
    
    M
    
    BiArg
    
    Node
    
    Edge
    
    Dot
    
    Make
    
    Query
    
    CfgNode
    
    Node
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    Witness
    
    M
    
    WitnessTaskResult
    
    Arg
    
    Node
    
    Edge
    
    Result
    
    Query
    
    ArgTool
    
    Query
    
    CfgNode
    
    Node
    
    NHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    NHT
    
    BiArgInvariant
    
    Node
    
    Edge
    
    Graphml
    
    GraphMlWriter
    
    StringGraphMlWriter
    
    XmlGraphMlWriter
    
    ArgNodeGraphMlWriter
    
    EnumerateNodeGraphMlWriter
    
    DeDupGraphMlWriter
    
    YamlWitness
    
    Entry
    
    Make
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    WitnessInvariant
    
    FMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    FCMap
    
    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
    
    Target
    
    Certification
    
    LoopInvariantCertificate
    
    PreconditionLoopInvariantCertificate
    
    EntryType
    
    Entry
    
    WideningTokens
    
    Token
    
    TS
    
    Dom
    
    Lifter
    
    D
    
    G
    
    C
    
    V
    
    P
    
    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
    
    Sarif
    
    SarifType
    
    Invocation
    
    Region
    
    ArtifactLocation
    
    PhysicalLocation
    
    Artifact
    
    Location
    
    Message
    
    ReportingDescriptor
    
    ToolComponent
    
    Tool
    
    Result
    
    Run
    
    SarifLog
    
    SarifRules
    
    Transform
    
    M
    
    S
    
    PartialEval
    
    visitor
    
    DeadCode
    
    RemoveDeadCode
    
    EvalAssert
    
    EvalAssert
    
    visitor
    
    ExpressionEvaluation
    
    ExpEval
    
    Timing
    
    Default
    
    Program
    
    GoblintDir
    
    IntOps
    
    IntOpsBase
    
    IntOps
    
    NIntOpsBase
    
    Int32OpsBase
    
    Int64OpsBase
    
    BigIntOpsBase
    
    IntOpsDecorator
    
    BigIntOps
    
    NIntOps
    
    Int32Ops
    
    Int64Ops
    
    FloatOps
    
    CFloatType
    
    CDouble
    
    CFloat
    
    LazyEval
    
    Make
    
    ResettableLazy
    
    ProcessPool
    
    Timeout
    
    Unix
    
    Js
    
    TimeUtil
    
    MessageUtil
    
    XmlUtil
    
    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
    
    addConstructors
    
    countFnVisitor
    
    StmtH
    
    VarinfoH
    
    StringH
    
    IntH
    
    stmtSidVisitor
    
    RichVarinfo
    
    VarinfoMap
    
    G
    
    H
    
    Make
    
    BiVarinfoMap
    
    S
    
    Collection
    
    Make
    
    CilCfg
    
    allBBVisitor
    
    countLoopsVisitor
    
    LoopUnrolling
    
    checkNoBreakVisitor
    
    findBreakVisitor
    
    isPointedAtVisitor
    
    hasAssignmentVisitor
    
    findAssignmentConstDiff
    
    arrayVisitor
    
    loopUnrollingCallVisitor
    
    StatementHashTable
    
    patchLabelsGotosVisitor
    
    copyandPatchLabelsVisitor
    
    loopUnrollingVisitor
    
    AccessKind
    
    LibraryDesc
    
    Cil
    
    Access
    
    Accesses
    
    MathPrintable
    
    MathLifted
    
    LibraryDsl
    
    LibraryFunctions
    
    BaseUtil
    
    PrecisionUtil
    
    ContextUtil
    
    BaseInvariant
    
    M
    
    VD
    
    ID
    
    FD
    
    AD
    
    BI
    
    Eval
    
    D
    
    V
    
    G
    
    Make
    
    CommonPriv
    
    Q
    
    IdxDom
    
    VD
    
    ConfCheck
    
    RequireMutexActivatedInit
    
    RequireMutexPathSensInit
    
    RequireThreadFlagPathSensInit
    
    Protection
    
    MutexGlobals
    
    VMutex
    
    Offs
    
    Mval
    
    VMutexInits
    
    VGlobal
    
    V
    
    MayVars
    
    MustVars
    
    Locksets
    
    Lock
    
    Lockset
    
    MustLockset
    
    MinLocksets
    
    WriteCenteredD
    
    W
    
    P
    
    PerMutexTidCommonArg
    
    PerMutexTidCommon
    
    TID
    
    W
    
    V
    
    LLock
    
    LMust
    
    L
    
    GMutex
    
    GThread
    
    G
    
    D
    
    WideningThresholds
    
    VectorMatrix
    
    Array
    
    M
    
    RatOps
    
    ConvenienceOps
    
    Vector
    
    AbstractVector
    
    Matrix
    
    AbstractMatrix
    
    ArrayVector
    
    ArrayMatrix
    
    SharedFunctions
    
    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
    
    ConfigOcaml
    
    ConfigProfile
    
    Version
    
    ConfigVersion
    
    GobFormat
    
    GobGc
    
    GobHashtbl
    
    Pretty
    
    GobList
    
    Syntax
    
    GobRef
    
    GobResult
    
    Syntax
    
    GobOption
    
    Syntax
    
    GobSys
    
    GobUnix
    
    GobFpath
    
    GobPretty
    
    GobYaml
    
    GobYojson
    
    GobZ
    
    MyCheck
    
    Gen
    
    Iter
    
    Shrink
    
    Arbitrary
- Library goblint.sites
  - Goblint_sites
- Library goblint.timing
  - Goblint_timing
    
    Name
    
    S
    
    Make
- Library goblint_build_info_dune
  - Goblint_build_info
- Library goblint_build_info_js
  - Goblint_build_info
- Library goblint_sites_dune
  - Goblint_sites
- Library goblint_sites_js
  - Goblint_sites
- Sources
  - goblint.backtrace
    
    goblint_backtrace.ml
  - goblint.lib
    
    affineEqualityAnalysis.ml
    
    affineEqualityDomain.ml
    
    apronAnalysis.ml
    
    apronDomain.ml
    
    apronPrecCompareUtil.ml
    
    autoTune.ml
    
    autoTune0.ml
    
    configOcaml.ml
    
    configProfile.ml
    
    configVersion.ml
    
    goblint_lib.ml
    
    goblint_lib__.ml
    
    maingoblint.ml
    
    relationAnalysis.ml
    
    relationDomain.ml
    
    relationPrecCompareUtil.ml
    
    relationPriv.ml
    
    sharedFunctions.ml
    
    version.ml
    
    violationZ3.ml
  - goblint.timing
    
    goblint_timing.ml
    
    goblint_timing__.ml
    
    goblint_timing_intf.ml
  - goblint_build_info_dune
    
    goblint_build_info.ml
    
    goblint_build_info__goblint_build_info_dune__.ml
  - goblint_build_info_js
    
    goblint_build_info.ml
    
    goblint_build_info__goblint_build_info_js__.ml
  - goblint_sites_dune
    
    goblint_sites.ml
    
    goblint_sites__goblint_sites_dune__.ml
  - goblint_sites_js
    
    goblint_sites.ml
    
    goblint_sites__goblint_sites_js__.ml

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

Module `WitnessUtil.InvariantExp`

module ES : sig ... end

val pullOutCommonConjuncts : GoblintCil.Cil.exp -> ES.t

val process_exp : GoblintCil.exp -> ES.elt list

package goblint

Module WitnessUtil.InvariantExp

Module `WitnessUtil.InvariantExp`