package goblint

You can search for identifiers within the package.

in-package search v0.2.0

package goblint

goblint
- Library goblint.lib
  - Goblint_lib
    
    AbstractionDomainProperties
    
    AbstractFunction
    
    AbstractTest
    
    Monotone
    
    ValidTest
    
    Access
    
    M
    
    A
    
    AS
    
    T
    
    O
    
    LV
    
    LVOpt
    
    AccessAnalysis
    
    M
    
    LF
    
    Spec
    
    A
    
    D
    
    C
    
    V0
    
    V
    
    V0Set
    
    G
    
    AccessKind
    
    AddressDomain
    
    GU
    
    M
    
    S
    
    AddressSet
    
    Addr
    
    Offs
    
    Map
    
    B
    
    AfterConfig
    
    Analyses
    
    GU
    
    M
    
    SysVar
    
    VarType
    
    Var
    
    VarF
    
    SpecSysVar
    
    GVarF
    
    GVarG
    
    CSet
    
    Dom
    
    ResultNode
    
    ResultConf
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    ControlSpecC
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    MCPA
    
    MCPSpec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    MonSystem
    
    Var
    
    Dom
    
    EqConstrSys
    
    Var
    
    Dom
    
    GlobConstrSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    GenericEqBoxIncrSolverBase
    
    IncrSolverArg
    
    GenericEqBoxIncrSolver
    
    GenericEqBoxSolver
    
    GenericGlobSolver
    
    ResultType2
    
    StdV
    
    VarinfoV
    
    EmptyV
    
    UnitA
    
    DefaultSpec
    
    G
    
    V
    
    A
    
    IdentitySpec
    
    G
    
    V
    
    A
    
    ApronAnalysis
    
    ApronDomain
    
    ApronPrecCompareUtil
    
    ApronPriv
    
    ArrayDomain
    
    S
    
    LatticeWithSmartOps
    
    Trivial
    
    TrivialWithLength
    
    Partitioned
    
    PartitionedWithLength
    
    FlagConfiguredArrayDomain
    
    Assert
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    Base
    
    A
    
    H
    
    Q
    
    GU
    
    ID
    
    FD
    
    IdxDom
    
    AD
    
    Addr
    
    Offs
    
    LF
    
    CArrays
    
    BI
    
    PU
    
    VD
    
    CPA
    
    Dep
    
    WeakUpdates
    
    BaseComponents
    
    MainFunctor
    
    A
    
    Dom
    
    D
    
    C
    
    V
    
    G
    
    MainSpec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    BaseDomain
    
    VD
    
    BI
    
    CPA
    
    M
    
    Glob
    
    Var
    
    Val
    
    PartDeps
    
    VarSet
    
    WeakUpdates
    
    BaseComponents
    
    ExpEvaluator
    
    DomFunctor
    
    DomWithTrivialExpEval
    
    BasePriv
    
    S
    
    D
    
    G
    
    V
    
    BaseUtil
    
    Basetype
    
    GU
    
    ExtractLocation
    
    Variables
    
    RawStrings
    
    Strings
    
    RawBools
    
    Bools
    
    CilExp
    
    CilStmt
    
    CilField
    
    BoolDomain
    
    Bool
    
    MayBool
    
    MustBool
    
    CfgTools
    
    H
    
    NH
    
    SCC
    
    CfgPrinters
    
    NodeStyles
    
    CfgPrinters
    
    CilMaps
    
    VarinfoOrdered
    
    VarinfoMap
    
    CilType
    
    S
    
    Std
    
    Location
    
    Varinfo
    
    Stmt
    
    Fundec
    
    Typ
    
    Compinfo
    
    Fieldinfo
    
    Exp
    
    Offset
    
    Lval
    
    Constant
    
    Cilfacade
    
    E
    
    GU
    
    allBBVisitor
    
    patchLabelsGotosVisitor
    
    StatementHashTable
    
    copyandPatchLabelsVisitor
    
    loopUnrollingVisitor
    
    addConstructors
    
    countFnVisitor
    
    StmtH
    
    VarinfoH
    
    StringH
    
    Cilfacade0
    
    CommonPriv
    
    Q
    
    IdxDom
    
    VD
    
    ProtectionLogging
    
    GM
    
    Exceptionless
    
    Infix
    
    Labels
    
    VarSet
    
    Protection
    
    MutexGlobals
    
    VMutex
    
    Offs
    
    VMutexInits
    
    VGlobal
    
    V
    
    MayVars
    
    MustVars
    
    Locksets
    
    Lock
    
    Lockset
    
    MustLockset
    
    MinLocksets
    
    WriteCenteredD
    
    W
    
    P
    
    ConfCheck
    
    RequireMutexActivatedInit
    
    RequireMutexPathSensInit
    
    RequireThreadFlagPathSensInit
    
    CompareAST
    
    StringMap
    
    GlobalMap
    
    CompareCFG
    
    StringMap
    
    GlobalMap
    
    NH
    
    CompareCIL
    
    StringMap
    
    GlobalMap
    
    NH
    
    VarinfoSet
    
    CompilationDatabase
    
    ConcDomain
    
    ThreadSet
    
    MustThreadSet
    
    CreatedThreadSet
    
    ThreadCreation
    
    UNames
    
    Uniqueness
    
    ParentThreadSet
    
    DirtyExitNames
    
    DirtyExit
    
    ThreadStringSet
    
    CondVars
    
    Domain
    
    V
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    ConfigProfile
    
    ConfigVersion
    
    Constants
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    Constraints
    
    M
    
    HashconsLifter
    
    D
    
    G
    
    C
    
    V
    
    HashconsContextLifter
    
    D
    
    G
    
    C
    
    V
    
    OptEqual
    
    D
    
    G
    
    C
    
    V
    
    LevelSliceLifter
    
    D
    
    G
    
    C
    
    V
    
    LimitLifter
    
    G
    
    C
    
    V
    
    H
    
    D
    
    WidenContextLifterSide
    
    DD
    
    M
    
    D
    
    G
    
    C
    
    V
    
    DeadCodeLifter
    
    D
    
    G
    
    C
    
    V
    
    Increment
    
    FromSpec
    
    LVar
    
    GVar
    
    D
    
    G
    
    EqIncrSolverFromEqSolver
    
    Var2
    
    EqConstrSysFromGlobConstrSys
    
    Var
    
    Dom
    
    GlobConstrSolFromEqConstrSolBase
    
    GlobConstrSolFromEqConstrSol
    
    S2
    
    Var
    
    Dom
    
    VH
    
    Exceptionless
    
    Infix
    
    Labels
    
    GlobSolverFromEqSolver
    
    PathSensitive2
    
    D
    
    G
    
    C
    
    V
    
    DeadBranchLifter
    
    D
    
    G
    
    C
    
    V
    
    CompareGlobSys
    
    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
    
    ContextUtil
    
    Control
    
    S2S
    
    D
    
    G
    
    C
    
    V
    
    AnalyzeCFG
    
    EQSys
    
    LVar
    
    GVar
    
    D
    
    G
    
    CSet
    
    LHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    GHT
    
    Exceptionless
    
    Infix
    
    Labels
    
    PostSolverArg
    
    Slvr
    
    CompareGlobSys
    
    G
    
    CSet
    
    PP
    
    Exceptionless
    
    Infix
    
    Labels
    
    RT
    
    LT
    
    Result
    
    Exceptionless
    
    Infix
    
    Labels
    
    WResult
    
    Deadlock
    
    Spec
    
    LockEventPair
    
    MayLockEventPairs
    
    Arg
    
    D
    
    V
    
    Offs
    
    G
    
    A
    
    D
    
    C
    
    V
    
    G
    
    DeadlockDomain
    
    Lock
    
    LockEvent
    
    MayLockEvents
    
    DomainProperties
    
    DomainTest
    
    S
    
    Equal
    
    Leq
    
    Join
    
    Meet
    
    Bot
    
    Top
    
    Connect
    
    Widen
    
    Narrow
    
    All
    
    AllNonAssoc
    
    Edge
    
    EffectWConEq
    
    Make
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    EscapeDomain
    
    EscapedVars
    
    EvalAssert
    
    EvalAssert
    
    visitor
    
    Events
    
    ExpDomain
    
    ExpRelation
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    ExpressionEvaluation
    
    ExpEval
    
    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
    
    A
    
    FileDomain
    
    D
    
    Val
    
    Dom
    
    K
    
    V
    
    MD
    
    FileUse
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    FlagHelper
    
    FlagError
    
    FlagHelper
    
    GroupableFlagHelper
    
    LatticeFlagHelperArg
    
    LatticeFlagHelper
    
    FlagModeDomain
    
    Eq
    
    Method
    
    L_names
    
    P
    
    Dom
    
    FloatDomain
    
    FloatArith
    
    FloatDomainBase
    
    F64Interval
    
    F32Interval
    
    FloatDomain
    
    FloatDomTupleImpl
    
    FloatOps
    
    CFloatType
    
    CDouble
    
    CFloat
    
    Generic
    
    LoadRunSolver
    
    LoadRunIncrSolver
    
    SolverStats
    
    GU
    
    DirtyBoxSolver
    
    SoundBoxSolverImpl
    
    GU
    
    SoundBoxSolver
    
    PreciseSideEffectBoxSolver
    
    GobConfig
    
    Validator
    
    ValidatorRequireAll
    
    S
    
    Impl
    
    GobFormat
    
    GobFpath
    
    GobHashtbl
    
    Pretty
    
    GobList
    
    GobOption
    
    GobSys
    
    GobUnix
    
    GobYaml
    
    GobYojson
    
    GoblintDir
    
    Goblintutil
    
    Graphml
    
    GraphMlWriter
    
    StringGraphMlWriter
    
    XmlGraphMlWriter
    
    ArgNodeGraphMlWriter
    
    EnumerateNodeGraphMlWriter
    
    DeDupGraphMlWriter
    
    HoareDomain
    
    Pretty
    
    HoarePO
    
    Map
    
    B
    
    SetS
    
    Set
    
    Set_LiftTop
    
    MapBot
    
    SpecDGroupable
    
    IntDomain
    
    Arith
    
    ArithIkind
    
    B
    
    IkindUnawareS
    
    S
    
    OldDomainFacade
    
    Y
    
    Z
    
    IntDomLifter
    
    Ikind
    
    PtrDiffIkind
    
    IntDomWithDefaultIkind
    
    IntDomTuple
    
    Size
    
    BISet
    
    Integers
    
    FlatPureIntegers
    
    Flattened
    
    FlattenedBI
    
    Lifted
    
    IntervalFunctor
    
    Interval32
    
    BigInt
    
    Interval
    
    Congruence
    
    DefExc
    
    Flat
    
    Lift
    
    Reverse
    
    Enums
    
    BooleansNames
    
    MakeBooleans
    
    Booleans
    
    IntDomainProperties
    
    BI
    
    OldS
    
    OldSWithIkind
    
    Ikind
    
    S
    
    WithIkind
    
    Ikind
    
    IntegerSet
    
    Base
    
    Valid
    
    All
    
    AllNonAssoc
    
    IntOps
    
    IntOpsBase
    
    IntOps
    
    NIntOpsBase
    
    Int32OpsBase
    
    Int64OpsBase
    
    BigIntOpsBase
    
    IntOpsDecorator
    
    BigIntOps
    
    NIntOps
    
    Int32Ops
    
    Int64Ops
    
    Invariant
    
    ExpLat
    
    N
    
    InvariantCil
    
    exp_replace_original_name_visitor
    
    exp_is_in_scope_visitor
    
    exp_contains_tmp_visitor
    
    JsonSchema
    
    JS
    
    JE
    
    JQ
    
    Schema
    
    Validator
    
    Lattice
    
    Pretty
    
    GU
    
    PO
    
    S
    
    UnitConf
    
    Unit
    
    Fake
    
    PD
    
    FakeSingleton
    
    Reverse
    
    HConsed
    
    HC
    
    HashCached
    
    LazyHash
    
    Flat
    
    Lift
    
    LiftPO
    
    Lift2
    
    ProdConf
    
    Prod
    
    ProdSimple
    
    Prod3
    
    LiftBot
    
    LiftTop
    
    Liszt
    
    Num
    
    ProdList
    
    Chain
    
    LazyEval
    
    Make
    
    LibraryDesc
    
    Cil
    
    Access
    
    Accesses
    
    LibraryDsl
    
    LibraryFunctionEffects
    
    LibraryFunctions
    
    LockDomain
    
    Addr
    
    Offs
    
    Equ
    
    Exp
    
    IdxDom
    
    Mutexes
    
    Simple
    
    Priorities
    
    Glob
    
    Var
    
    Val
    
    Lockset
    
    RW
    
    Lock
    
    ReverseAddrSet
    
    AddrSet
    
    MayLockset
    
    RW
    
    Lock
    
    ReverseAddrSet
    
    AddrSet
    
    Symbolic
    
    S
    
    LocksetAnalysis
    
    DS
    
    Make
    
    G
    
    V
    
    A
    
    D
    
    C
    
    MayArg
    
    D
    
    G
    
    V
    
    MakeMay
    
    A
    
    D
    
    C
    
    G
    
    V
    
    MustArg
    
    D
    
    G
    
    V
    
    MakeMust
    
    A
    
    D
    
    C
    
    G
    
    V
    
    Lval
    
    GU
    
    IdxDomain
    
    OffsetPrintable
    
    Offset
    
    S
    
    Normal
    
    Offs
    
    NormalLat
    
    Offs
    
    Fields
    
    F
    
    I
    
    FI
    
    CilLval
    
    LvalMapDomain
    
    M
    
    S
    
    Value
    
    Domain
    
    K
    
    V
    
    MD
    
    MCP
    
    DomainListPrintableSpec
    
    DomainListSysVarSpec
    
    DomainListMCPASpec
    
    DomainListLatticeSpec
    
    PrintableOfLatticeSpec
    
    PrintableOfMCPASpec
    
    PrintableOfSysVarSpec
    
    DomListPrintable
    
    DomVariantPrintable
    
    DomVariantSysVar
    
    DomListLattice
    
    DomVariantLattice0
    
    DomVariantLattice
    
    LocalDomainListSpec
    
    GlobalDomainListSpec
    
    ContextListSpec
    
    VarListSpec
    
    AccListSpec
    
    MCP2
    
    D
    
    G
    
    C
    
    V
    
    MCPAccess
    
    Pretty
    
    A
    
    MCPRegistry
    
    DomainListPrintableSpec
    
    DomainListSysVarSpec
    
    DomainListMCPASpec
    
    DomainListLatticeSpec
    
    PrintableOfLatticeSpec
    
    PrintableOfMCPASpec
    
    PrintableOfSysVarSpec
    
    DomListPrintable
    
    DomVariantPrintable
    
    DomVariantSysVar
    
    DomListLattice
    
    DomVariantLattice0
    
    DomVariantLattice
    
    LocalDomainListSpec
    
    GlobalDomainListSpec
    
    ContextListSpec
    
    VarListSpec
    
    AccListSpec
    
    MHP
    
    TID
    
    Pretty
    
    MHPAnalysis
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    TID
    
    Pretty
    
    Maingoblint
    
    MakefileUtil
    
    MallocFresh
    
    Spec
    
    G
    
    V
    
    D
    
    C
    
    A
    
    MallocWrapperAnalysis
    
    Q
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    Malloc_null
    
    AD
    
    IdxDom
    
    Offs
    
    Spec
    
    G
    
    V
    
    A
    
    Addr
    
    D
    
    C
    
    MapDomain
    
    Pretty
    
    ME
    
    GU
    
    PS
    
    S
    
    Groupable
    
    PMap
    
    HashCached
    
    HConsed
    
    Timed
    
    MapBot
    
    MapTop
    
    LiftTop
    
    MapBot_LiftTop
    
    LiftBot
    
    MapTop_LiftBot
    
    MaxIdUtil
    
    MayLocks
    
    Arg
    
    D
    
    G
    
    V
    
    Spec
    
    A
    
    D
    
    C
    
    G
    
    V
    
    MessageCategory
    
    Behavior
    
    Undefined
    
    ArrayOutOfBounds
    
    Integer
    
    Cast
    
    MessageUtil
    
    Messages
    
    Pretty
    
    GU
    
    Category
    
    Severity
    
    Location
    
    Piece
    
    MultiPiece
    
    Tag
    
    Tags
    
    Message
    
    Table
    
    MH
    
    Strs
    
    MusteqDomain
    
    V
    
    F
    
    F
    
    I
    
    FI
    
    EquAddr
    
    P
    
    Equ
    
    MutexAnalysis
    
    M
    
    Addr
    
    Lockset
    
    Mutexes
    
    LF
    
    SpecParam
    
    G
    
    MakeSpec
    
    Arg
    
    D
    
    G
    
    V
    
    C
    
    D
    
    G
    
    V
    
    A
    
    RW
    
    Lock
    
    ReverseAddrSet
    
    AddrSet
    
    WriteBased
    
    GReadWrite
    
    GWrite
    
    G
    
    Spec
    
    Arg
    
    D
    
    G
    
    V
    
    C
    
    D
    
    G
    
    V
    
    A
    
    RW
    
    Lock
    
    ReverseAddrSet
    
    AddrSet
    
    MutexEventsAnalysis
    
    M
    
    Addr
    
    Lockset
    
    Mutexes
    
    LF
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    MyARG
    
    Node
    
    Edge
    
    CFGEdge
    
    InlineEdge
    
    S
    
    Node
    
    Edge
    
    StackNode
    
    Stack
    
    Node
    
    Edge
    
    IsInteresting
    
    InterestingArg
    
    Node
    
    Edge
    
    SIntra
    
    SIntraOpt
    
    CfgIntra
    
    UnCilLogicIntra
    
    UnCilTernaryIntra
    
    Intra
    
    Node
    
    Edge
    
    MyCFG
    
    CfgBackward
    
    CfgForward
    
    CfgBidir
    
    NodeH
    
    Exceptionless
    
    Infix
    
    Labels
    
    MyCheck
    
    Gen
    
    Iter
    
    Shrink
    
    Arbitrary
    
    Node
    
    Node0
    
    ObserverAnalysis
    
    StepObserverAutomaton
    
    MakeSpec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    PathArg
    
    MakePathSpec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    ObserverAutomaton
    
    S
    
    KMPArg
    
    KMP
    
    Options
    
    PartitionDomain
    
    Collapse
    
    Set
    
    CollapseSet
    
    Make
    
    S
    
    SetSet
    
    B
    
    E
    
    ExpPartitions
    
    B
    
    E
    
    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
    
    PreValueDomain
    
    ID
    
    FD
    
    IndexDomain
    
    AD
    
    Addr
    
    Offs
    
    Map
    
    B
    
    Addr
    
    Offs
    
    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
    
    PrecisionUtil
    
    Prelude
    
    All
    
    Legacy
    
    LargeFile
    
    Arg
    
    Array
    
    ArrayLabels
    
    Buffer
    
    Bytes
    
    Callback
    
    Char
    
    Complex
    
    Digest
    
    Either
    
    Filename
    
    Format
    
    Gc
    
    Genlex
    
    Hashtbl
    
    Int32
    
    Int64
    
    Lazy
    
    Lexing
    
    List
    
    ListLabels
    
    Map
    
    Marshal
    
    MoreLabels
    
    Nativeint
    
    Oo
    
    Parsing
    
    Printexc
    
    Printf
    
    Queue
    
    Random
    
    Scanf
    
    Set
    
    Seq
    
    Stack
    
    StdLabels
    
    Stream
    
    String
    
    StringLabels
    
    Sys
    
    Weak
    
    Unix
    
    Num
    
    Big_int
    
    Bigarray
    
    Str
    
    Result
    
    Array
    
    Buffer
    
    Bytes
    
    Char
    
    Complex
    
    Digest
    
    Either
    
    Gc
    
    Genlex
    
    Hashtbl
    
    Int32
    
    Int64
    
    Lexing
    
    List
    
    Map
    
    Marshal
    
    Nativeint
    
    Printexc
    
    Printf
    
    Queue
    
    Random
    
    Scanf
    
    Set
    
    Stack
    
    Stream
    
    String
    
    Sys
    
    Unix
    
    Big_int
    
    Num
    
    Bigarray
    
    Base64
    
    BitSet
    
    Bit_set
    
    Dllist
    
    DynArray
    
    Enum
    
    File
    
    Global
    
    IO
    
    LazyList
    
    MultiPMap
    
    Option
    
    RefList
    
    Ref
    
    Cache
    
    CharParser
    
    Deque
    
    Hashcons
    
    Heap
    
    FingerTree
    
    Logger
    
    MultiMap
    
    ParserCo
    
    Result
    
    Return
    
    Seq
    
    Substring
    
    Tuple
    
    Tuple2
    
    Tuple3
    
    Tuple4
    
    Tuple5
    
    Vect
    
    ISet
    
    IMap
    
    Splay
    
    Uref
    
    UChar
    
    UTF8
    
    Text
    
    Concurrent
    
    Interfaces
    
    Number
    
    Float
    
    Int
    
    Bool
    
    Unit
    
    Filename
    
    Incubator
    
    Log
    
    Bounded
    
    PathGen
    
    LargeFile
    
    Format
    
    Legacy
    
    Array
    
    Buffer
    
    Bytes
    
    Char
    
    Complex
    
    Digest
    
    Either
    
    Gc
    
    Genlex
    
    Hashtbl
    
    Int32
    
    Int64
    
    Lexing
    
    List
    
    Map
    
    Marshal
    
    Nativeint
    
    Printexc
    
    Printf
    
    Queue
    
    Random
    
    Scanf
    
    Set
    
    Stack
    
    Stream
    
    String
    
    Sys
    
    Unix
    
    Big_int
    
    Num
    
    Bigarray
    
    Base64
    
    BitSet
    
    Bit_set
    
    Dllist
    
    DynArray
    
    Enum
    
    File
    
    Global
    
    IO
    
    LazyList
    
    MultiPMap
    
    Option
    
    RefList
    
    Ref
    
    Cache
    
    CharParser
    
    Deque
    
    Hashcons
    
    Heap
    
    FingerTree
    
    Logger
    
    MultiMap
    
    ParserCo
    
    Result
    
    Return
    
    Seq
    
    Substring
    
    Tuple
    
    Tuple2
    
    Tuple3
    
    Tuple4
    
    Tuple5
    
    Vect
    
    ISet
    
    IMap
    
    Splay
    
    Uref
    
    UChar
    
    UTF8
    
    Text
    
    Concurrent
    
    Interfaces
    
    Number
    
    Float
    
    Int
    
    Bool
    
    Unit
    
    Filename
    
    Incubator
    
    LargeFile
    
    Format
    
    Ana
    
    Legacy
    
    Array
    
    Buffer
    
    Bytes
    
    Char
    
    Complex
    
    Digest
    
    Either
    
    Gc
    
    Genlex
    
    Hashtbl
    
    Int32
    
    Int64
    
    Lexing
    
    List
    
    Map
    
    Marshal
    
    Nativeint
    
    Printexc
    
    Printf
    
    Queue
    
    Random
    
    Scanf
    
    Set
    
    Stack
    
    Stream
    
    String
    
    Sys
    
    Unix
    
    Big_int
    
    Num
    
    Bigarray
    
    Base64
    
    BitSet
    
    Bit_set
    
    Dllist
    
    DynArray
    
    Enum
    
    File
    
    Global
    
    IO
    
    LazyList
    
    MultiPMap
    
    Option
    
    RefList
    
    Ref
    
    Cache
    
    CharParser
    
    Deque
    
    Hashcons
    
    Heap
    
    FingerTree
    
    Logger
    
    MultiMap
    
    ParserCo
    
    Result
    
    Return
    
    Seq
    
    Substring
    
    Tuple
    
    Tuple2
    
    Tuple3
    
    Tuple4
    
    Tuple5
    
    Vect
    
    ISet
    
    IMap
    
    Splay
    
    Uref
    
    UChar
    
    UTF8
    
    Text
    
    Concurrent
    
    Interfaces
    
    Number
    
    Float
    
    Int
    
    Bool
    
    Unit
    
    Filename
    
    Incubator
    
    LargeFile
    
    Format
    
    cilVisitor
    
    nopCilVisitor
    
    cilPrinter
    
    defaultCilPrinterClass
    
    plainCilPrinterClass
    
    descriptiveCilPrinter
    
    descriptiveCilPrinterClass
    
    Cfg
    
    Check
    
    Cil
    
    Cilint
    
    Cillower
    
    Ciltools
    
    Cilutil
    
    Dataflow
    
    Dominators
    
    Escape
    
    Expcompare
    
    Feature
    
    Formatcil
    
    Machdep
    
    Machdepenv
    
    Mergecil
    
    Rmtmps
    
    Cabs
    
    Cabs2cil
    
    Cabshelper
    
    Cabsvisit
    
    Cprint
    
    Frontc
    
    Patch
    
    Whitetrack
    
    Alpha
    
    Errormsg
    
    GrowArray
    
    Inthash
    
    Pretty
    
    Stats
    
    Trace
    
    Util
    
    MakeMapPrinter
    
    MakeSetPrinter
    
    Preprocessor
    
    FpathH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Printable
    
    Pretty
    
    S
    
    Empty
    
    Std
    
    Blank
    
    Showable
    
    SimpleShow
    
    Prettyable
    
    SimplePretty
    
    Name
    
    UnitConf
    
    Unit
    
    LiftingNames
    
    DefaultNames
    
    HConsed
    
    HC
    
    HashCached
    
    LazyHash
    
    Lift
    
    Either
    
    Option
    
    Lift2
    
    ProdConfiguration
    
    ProdConf
    
    Prod
    
    ProdSimple
    
    Prod3
    
    Liszt
    
    ChainParams
    
    Chain
    
    LiftBot
    
    LiftTop
    
    Strings
    
    FailwithMessage
    
    Failwith
    
    PrivPrecCompareUtil
    
    LV
    
    Util
    
    Key
    
    Dom
    
    RH
    
    Exceptionless
    
    Infix
    
    Labels
    
    Key
    
    Dom
    
    RH
    
    ProcessPool
    
    PthreadDomain
    
    Tid
    
    Ctx
    
    Pred
    
    Base
    
    D
    
    Queries
    
    GU
    
    ID
    
    I
    
    LS
    
    TS
    
    ES
    
    VI
    
    SD
    
    MayBool
    
    MustBool
    
    Unit
    
    Result
    
    Any
    
    Set
    
    Exceptionless
    
    Labels
    
    Hashtbl
    
    Exceptionless
    
    Infix
    
    Labels
    
    Refinement
    
    Region
    
    RegMap
    
    RegPart
    
    Reg
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    Lvals
    
    A
    
    RegionDomain
    
    GU
    
    V
    
    B
    
    F
    
    VF
    
    VFB
    
    RS
    
    RegPart
    
    S
    
    RegMap
    
    Reg
    
    RegionDom
    
    ResettableLazy
    
    RichVarinfo
    
    VarinfoMap
    
    G
    
    H
    
    Make
    
    BiVarinfoMap
    
    S
    
    Collection
    
    Make
    
    SLR
    
    SLR3
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Version
    
    Make
    
    X
    
    XY
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    H
    
    HeapCompare
    
    L
    
    P
    
    T
    
    D
    
    MyGenericEqBoxSolver
    
    X
    
    PrintInfluence
    
    S1
    
    X
    
    TwoPhased
    
    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
    
    SLRphased
    
    Make
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    SLRterm
    
    SLR3term
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    Sarif
    
    SarifRules
    
    SarifType
    
    Invocation
    
    Region
    
    ArtifactLocation
    
    PhysicalLocation
    
    Artifact
    
    Location
    
    Message
    
    ReportingDescriptor
    
    ToolComponent
    
    Tool
    
    Result
    
    Run
    
    SarifLog
    
    Selector
    
    Make
    
    Serialize
    
    Cache
    
    Server
    
    Request
    
    Registry
    
    ParamParser
    
    Function
    
    SetDomain
    
    Pretty
    
    S
    
    Make
    
    SensitiveConf
    
    Elt
    
    Sensitive
    
    Elt
    
    ToppedSetNames
    
    LiftTop
    
    ToppedSet
    
    HeadlessSet
    
    Reverse
    
    FiniteSetElems
    
    FiniteSet
    
    E
    
    Signs
    
    Signs
    
    SL
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    Spec
    
    SC
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    SpecCheck
    
    SpecCore
    
    SpecDomain
    
    D
    
    Val
    
    Dom
    
    K
    
    V
    
    MD
    
    SpecLexer
    
    SpecParser
    
    SpecUtil
    
    StackDomain
    
    GU
    
    S
    
    Dom1
    
    VarLat
    
    Var
    
    Dom2
    
    Var
    
    Loc
    
    Dom3
    
    StackTrace
    
    LF
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    SpecLoc
    
    G
    
    V
    
    A
    
    D
    
    C
    
    Spec1
    
    G
    
    V
    
    A
    
    D
    
    C
    
    Spec2
    
    G
    
    V
    
    A
    
    D
    
    C
    
    StructDomain
    
    Arg
    
    S
    
    Simple
    
    Sets
    
    KeyedSets
    
    FlagConfiguredStructDomain
    
    Svcomp
    
    Specification
    
    Task
    
    Cfg
    
    Result
    
    TaskResult
    
    Arg
    
    Node
    
    Edge
    
    StackTaskResult
    
    Arg
    
    Node
    
    Edge
    
    SymbLocks
    
    LF
    
    LP
    
    Exp
    
    ILock
    
    VarEq
    
    PS
    
    Spec
    
    G
    
    V
    
    D
    
    C
    
    A
    
    E
    
    SymbLocksDomain
    
    M
    
    Exp
    
    LockingPattern
    
    ILock
    
    Idx
    
    Offs
    
    Taint
    
    VarinfoSet
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    Td3
    
    WP
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    CurrentVarS
    
    S
    
    Var
    
    Dom
    
    S
    
    Termination
    
    M
    
    TermDomain
    
    loopCounterVisitor
    
    loopBreaksVisitor
    
    loopVarsVisitor
    
    loopInstrVisitor
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    C
    
    recomputeVisitor
    
    ThreadAnalysis
    
    T
    
    TS
    
    Spec
    
    A
    
    D
    
    C
    
    G
    
    V
    
    D
    
    ThreadEscape
    
    M
    
    Spec
    
    A
    
    D
    
    C
    
    V
    
    G
    
    ThreadFlag
    
    GU
    
    LF
    
    Spec
    
    G
    
    V
    
    Flag
    
    D
    
    C
    
    A
    
    ThreadFlagDomain
    
    S
    
    Trivial
    
    Simple
    
    ThreadId
    
    GU
    
    LF
    
    Thread
    
    ThreadLifted
    
    Spec
    
    G
    
    V
    
    TD
    
    D
    
    C
    
    A
    
    ThreadIdDomain
    
    S
    
    Stateless
    
    Stateful
    
    D
    
    FunNode
    
    Unit
    
    D
    
    History
    
    D
    
    ThreadLiftNames
    
    Lift
    
    FlagConfiguredTID
    
    D
    
    Thread
    
    ThreadLifted
    
    ThreadJoins
    
    TID
    
    TIDs
    
    MustTIDs
    
    Spec
    
    A
    
    D
    
    C
    
    G
    
    V
    
    D
    
    ThreadReturn
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    TimeUtil
    
    Timeout
    
    Unix
    
    Js
    
    TopDown
    
    WP
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    TopDown_deprecated
    
    GU
    
    TD3
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    HPM
    
    Exceptionless
    
    Infix
    
    Labels
    
    TopDown_space_cache_term
    
    WP
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    TopDown_term
    
    WP
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    P
    
    Tracing
    
    Strs
    
    Transform
    
    S
    
    PartialEval
    
    visitor
    
    Uninit
    
    M
    
    AD
    
    IdxDom
    
    Offs
    
    Spec
    
    G
    
    V
    
    A
    
    Addr
    
    D
    
    C
    
    UnionDomain
    
    Arg
    
    S
    
    Field
    
    Simple
    
    UnitAnalysis
    
    Spec
    
    D
    
    G
    
    C
    
    V
    
    A
    
    UpdateCil
    
    NodeMap
    
    UpdateCil0
    
    NodeMap
    
    ValueDomain
    
    ID
    
    FD
    
    IndexDomain
    
    AD
    
    Addr
    
    Offs
    
    M
    
    GU
    
    Expp
    
    Q
    
    BI
    
    AddrSetDomain
    
    ArrIdxDomain
    
    S
    
    Blob
    
    ZeroInit
    
    Blob
    
    Threads
    
    Compound
    
    Structs
    
    Unions
    
    CArrays
    
    Blobs
    
    VarEq
    
    Addr
    
    Offs
    
    AD
    
    Exp
    
    LF
    
    Spec
    
    G
    
    V
    
    A
    
    D
    
    B
    
    E
    
    C
    
    VarQuery
    
    Version
    
    Violation
    
    ViolationArg
    
    Node
    
    Edge
    
    Feasibility
    
    Node
    
    UnknownFeasibility
    
    Node
    
    PathArg
    
    Node
    
    Edge
    
    ViolationZ3
    
    WP
    
    WideningThresholds
    
    Witness
    
    Stats
    
    WitnessTaskResult
    
    Arg
    
    Node
    
    Edge
    
    Result
    
    WitnessConstraints
    
    Node
    
    Edge
    
    PathSensitive3
    
    D
    
    G
    
    C
    
    V
    
    WitnessUtil
    
    NH
    
    NS
    
    File
    
    Invariant
    
    InvariantExp
    
    ES
    
    InvariantParser
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    Worklist
    
    Make
    
    GU
    
    VS
    
    Exceptionless
    
    Labels
    
    XmlUtil
    
    YamlWitness
    
    Entry
    
    Query
    
    Make
    
    NH
    
    Exceptionless
    
    Infix
    
    Labels
    
    WitnessInvariant
    
    FMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    FCMap
    
    Exceptionless
    
    Infix
    
    Labels
    
    Query
    
    ValidationResult
    
    ChainParams
    
    Validator
    
    Locator
    
    FileH
    
    Exceptionless
    
    Infix
    
    Labels
    
    LocM
    
    Exceptionless
    
    Infix
    
    Labels
    
    ES
    
    Exceptionless
    
    Labels
    
    LvarS
    
    InvariantParser
    
    VR
    
    Query
    
    YamlWitnessType
    
    Producer
    
    Task
    
    Metadata
    
    Location
    
    Invariant
    
    LoopInvariant
    
    PreconditionLoopInvariant
    
    Target
    
    Certification
    
    LoopInvariantCertificate
    
    PreconditionLoopInvariantCertificate
    
    EntryType
    
    Entry
- Library goblint.sites
  - Goblint_sites
- Library goblint_sites_dune
  - Goblint_sites
- Library goblint_sites_js
  - Goblint_sites
- Sources
  - goblint.lib
    
    apronAnalysis.ml
    
    apronDomain.ml
    
    apronPrecCompareUtil.ml
    
    apronPriv.ml
    
    configProfile.ml
    
    configVersion.ml
    
    goblint_lib.ml
    
    maingoblint.ml
    
    prelude.ml
    
    version.ml
    
    violationZ3.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 `MakeSpec.Arg`

module D = Lockset

module G = P.G

module V = Analyses.VarinfoV

val add : 
  (D.ReverseAddrSet.t, 'a, 'b, 'c) Analyses.ctx ->
  (Goblint_lib.ValueDomain.Addr.t * D.RW.t) ->
  D.ReverseAddrSet.t

val remove : 
  (D.ReverseAddrSet.t, 'a, 'b, 'c) Analyses.ctx ->
  Goblint_lib.ValueDomain.Addr.t ->
  D.ReverseAddrSet.t

val remove_all : 'a -> D.ReverseAddrSet.t

package goblint

Module MakeSpec.Arg

Module `MakeSpec.Arg`