package mopsa

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Header of the abstraction
Lattice operators
Forward semantics
Backward semantics
Pretty printer

package mopsa

mopsa.c_stubs_parser
- Mopsa_c_stubs_parser
  - Main
mopsa.mopsa_analyzer
- Mopsa_analyzer
mopsa.mopsa_analyzer.c
- C
mopsa.mopsa_analyzer.c.common
- C_common
  - Common
    
    Alarms
    
    Base
    
    Base
    
    BaseMap
    
    BaseSet
    
    Builtins
    
    Points_to
    
    PointsToMap
    
    PointsToSet
    
    Quantified_offset
    
    Scope_update
    
    Soundness
mopsa.mopsa_analyzer.c.lang
- C_lang
  - Lang
    
    Ast
    
    CProgramKey
    
    TargetCtx
    
    Frontend
    
    Pp
    
    Visitor
mopsa.mopsa_analyzer.cfg
- Cfg
  - Ast
    
    CFG
    
    EdgeMap
    
    EdgeSet
    
    NodeMap
    
    NodeSet
    
    P
    
    EdgeId
    
    NodeId
    
    Port
    
    CFG_Param
    
    Loc
    
    LocHash
    
    LocMap
    
    LocSet
    
    Port
    
    Range
    
    RangeHash
    
    RangeMap
    
    RangeSet
    
    TagLoc
    
    TagLocHash
    
    TagLocMap
    
    TagLocSet
  - Frontend
  - Iterator
    
    Domain
  - Pp
  - Visitor
mopsa.mopsa_analyzer.cpyton
- Cpython
  - Alarms
  - Callstack_tracking
    
    Domain
    
    CallstackMap
    
    Callstacks
    
    CallstackSet
    
    Set
  - Cmodule
    
    AddrSet
    
    Set
    
    Domain
    
    EquivBaseAddrs
    
    NoAddrBase
    
    OtherMap
    
    KeySet
    
    ValueSet
  - Count_transitions
    
    Hook
  - Prelude
  - Soundness
mopsa.mopsa_analyzer.framework
- Framework
  - Runner
mopsa.mopsa_analyzer.framework.combiners
- Combiners
mopsa.mopsa_analyzer.framework.combiners.common
- Combiners_common
  - Common
mopsa.mopsa_analyzer.framework.combiners.domain
- Domain
  - Apply
    
    Make
    
    D1
    
    D2
  - Compose
    
    Make
    
    D1
    
    D2
  - Domain_switch
    
    Make
    
    D1
    
    D2
  - Product
  - Simplified_product
  - Stateless_switch
    
    Make
    
    D1
    
    D2
  - Switch
    
    Make
    
    D1
    
    D2
mopsa.mopsa_analyzer.framework.combiners.value
- Value
  - Nonrel
    
    Make
    
    Value
  - Product
    
    Make
    
    R
    
    V
    
    MakeValuePair
    
    V1
    
    V2
  - Union
    
    Make
    
    V1
    
    V2
mopsa.mopsa_analyzer.framework.core
- Core
  - Alarm
    
    AlarmSet
    
    AssumptionSet
    
    CallstackSet
    
    CheckMap
    
    RangeCallStackMap
    
    RangeDiagnosticWoCsMap
    
    RangeMap
  - All
    
    Var
  - Avalue
  - Cache
    
    KEY
    
    Make
    
    Domain
    
    EvalCache
    
    ExecCache
    
    Queue
    
    Key
  - Cases
  - Context
    
    GenContextKey
    
    Value
  - Effect
  - Eval
  - Flow
  - Hook
    
    HOOK
    
    STATELESS_HOOK
  - Id
    
    GenDomainId
    
    Spec
    
    GenStatelessDomainId
    
    Spec
    
    GenValueId
    
    Spec
  - Lattice
    
    LATTICE
  - Manager
  - Post
  - Print
  - Query
  - Route
    
    DomainSet
  - Token
    
    TokenMap
  - Utils
mopsa.mopsa_analyzer.framework.core.ast
- Ast
  - Addr
  - Constant
  - Expr
    
    ExprMap
    
    ExprSet
  - Frontend
  - Operator
  - Program
  - Semantic
    
    SemanticMap
    
    SemanticSet
  - Stmt
    
    StmtMap
    
    StmtSet
  - Typ
  - Var
    
    VarMap
    
    VarSet
  - Visitor
mopsa.mopsa_analyzer.framework.engines
- Engines
  - Automatic
    
    Make
    
    Toplevel
  - Engine_sig
    
    ENGINE
mopsa.mopsa_analyzer.framework.interactive
- Interactive
  - Action
  - Breakpoint
    
    BreakpointSet
  - Dap
    
    Make
    
    Toplevel
  - Engine
    
    Make
    
    Interface
    
    InterfaceFunctor
    
    Toplevel
    
    Toplevel
  - Envdb
    
    CallstackMap
  - Interface
    
    INTERFACE
    
    Toplevel
  - Query
  - Terminal
    
    Make
    
    Addr
    
    AddrSet
    
    Toplevel
  - Trace
mopsa.mopsa_analyzer.framework.lattices
- Lattices
  - Pair
    
    Make
    
    First
    
    Second
    
    ORDER
  - Partial_inversible_map
    
    Make
    
    Key
    
    Value
    
    ORDER
  - Partial_inversible_map_sig
    
    S
    
    KeySet
    
    ValueSet
  - Partial_map
    
    KEY
    
    Make
    
    Key
    
    Value
  - Pointwise
    
    KEY
    
    Make
    
    Key
    
    M
    
    Value
  - Powerset
    
    ELT
    
    Make
    
    Elt
  - Powerset_sig
    
    S
    
    Set
  - Powersetwithunder
    
    ELT
    
    Make
    
    Elt
    
    Set
    
    USet
    
    Set
mopsa.mopsa_analyzer.framework.output
- Output
  - Common
    
    OUTPUT
  - Factory
  - Json
    
    AlarmKindSet
  - Text
    
    AlarmKindSet
mopsa.mopsa_analyzer.framework.params
- Params
  - Options
  - Paths
mopsa.mopsa_analyzer.framework.params.config
- Config
  - Builder
  - Parser
  - Syntax
  - Visitor
mopsa.mopsa_analyzer.framework.sig
- Sig
mopsa.mopsa_analyzer.framework.sig.abstraction
- Abstraction
  - Domain
    
    DOMAIN
  - Functor
    
    DOMAIN_FUNCTOR
    
    Functor
    
    D
  - Simplified
    
    SIMPLIFIED
  - Simplified_functor
    
    SIMPLIFIED_FUNCTOR
    
    Functor
    
    D
  - Simplified_value
    
    DefaultValueFunctions
    
    MakeValue
    
    V
    
    SIMPLIFIED_VALUE
  - Stacked
    
    STACKED
  - Stateless
    
    STATELESS
  - Value
    
    DefaultValueFunctions
    
    VALUE
  - Value_functor
    
    VALUE_FUNCTOR
    
    Functor
    
    D
mopsa.mopsa_analyzer.framework.sig.combiner
- Combiner
  - Domain
    
    DOMAIN_COMBINER
    
    DomainToCombiner
    
    D
    
    StackedToStandard
    
    D
    
    StandardToStacked
    
    D
  - Simplified
    
    CombinerToSimplified
    
    T
    
    SIMPLIFIED_COMBINER
    
    SimplifiedToCombiner
    
    D
    
    SimplifiedToStandard
    
    D
  - Simplified_functor
    
    SIMPLIFIED_FUNCTOR
    
    Functor
    
    D
  - Stacked
    
    CombinerToStacked
    
    T
    
    EmptyDomain
    
    STACKED_COMBINER
    
    StackedToCombiner
    
    D
  - Stateless
    
    CombinerToStateless
    
    T
    
    STATELESS_COMBINER
    
    StatelessToCombiner
    
    D
    
    StatelessToDomain
    
    S
mopsa.mopsa_analyzer.framework.sig.reduction
- Reduction
mopsa.mopsa_analyzer.framework.toplevel
- Toplevel
  - Make
    
    Domain
  - TOPLEVEL
mopsa.mopsa_analyzer.mopsa
- Mopsa
mopsa.mopsa_analyzer.pyhton.lang
- Python_lang
  - Lang
    
    Addr
    
    Alarms
    
    Ast
    
    K
    
    Ast_compare
    
    Operators
    
    Pp
    
    Utils
    
    Visitor
mopsa.mopsa_analyzer.python
- Python
mopsa.mopsa_analyzer.repl
- Repl
  - Frontend
    
    Domain
mopsa.mopsa_analyzer.stubs
- Stubs
  - Alarms
  - Ast
  - Body
    
    Domain
  - Fallback
    
    Domain
  - Soundness
mopsa.mopsa_analyzer.universal
- Universal
mopsa.mopsa_analyzer.universal.heap
- Heap
  - Policies
  - Recency
    
    Domain
    
    Pool
    
    Set
mopsa.mopsa_analyzer.universal.hooks
- Hooks
  - Constant_widening_thresholds
    
    Hook
    
    ThresholdSet
  - Function_profiler
    
    Hook
  - Gctest
    
    Hook
  - Logs
    
    Hook
    
    Options
    
    OPTIONS
  - Loop_profiler
    
    Hook
    
    LoopMap
  - Progress
    
    Hook
    
    RangeSet
mopsa.mopsa_analyzer.universal.iterators
- Universal_iterators
  - Iterators
    
    Intraproc
    
    Domain
    
    Loops
    
    Domain
    
    LastFixpointCtx
    
    LoopHeadMap
    
    Program
    
    Domain
    
    Unittest
    
    Domain
mopsa.mopsa_analyzer.universal.iterators.interproc
- Universal_interproc
  - Interproc
    
    Common
    
    ReturnKey
    
    Inlining
    
    Domain
    
    Sequential_cache
    
    Domain
    
    Fctx
mopsa.mopsa_analyzer.universal.lang
- Lang
  - Ast
    
    Addr
    
    AddrSet
    
    UProgramKey
  - Frontend
    
    NameG
mopsa.mopsa_analyzer.universal.numeric
- Universal_numeric
  - Numeric
mopsa.mopsa_analyzer.universal.numeric.common
- Numeric_common
  - Common
    
    K
mopsa.mopsa_analyzer.universal.numeric.relational
- Relational
  - Apron_manager
    
    APRONMANAGER
  - Apron_pp
  - Apron_transformer
    
    ApronTransformer
    
    ApronManager
  - Binding
    
    Equiv
    
    LR
    
    RL
  - Domain
    
    Make
    
    ApronManager
  - Elinainst
  - Instances
    
    LinEqualities
    
    Octagon
    
    Polyhedra
    
    RELATIONAL
  - Instances_choices
  - Ppliteinst
mopsa.mopsa_analyzer.universal.numeric.values
- Numeric_values
  - Values
    
    Congruences
    
    Value
    
    Zero
    
    Value
mopsa.mopsa_analyzer.universal.numeric.values.intervals
- Intervals
  - Float
    
    SimplifiedValue
    
    Value
    
    V
  - Integer
    
    SimplifiedValue
    
    Value
    
    V
mopsa.mopsa_analyzer.universal.numeric.values.powersets
- Powersets
  - Excluded
    
    SimplifiedValue
    
    Set
  - Standard
    
    Value
    
    Powerset
    
    Set
mopsa.mopsa_analzyer.universal.numeric.reductions
- Numeric_reductions
mopsa.mopsa_build_db
- Mopsa_build_db
  - StringMap
mopsa.mopsa_c_parser
- Mopsa_c_parser
  - C_AST
    
    RangeMap
    
    StringMap
    
    UidMap
    
    UidSet
  - C_parser
  - C_print
  - C_simplify
  - C_utils
    
    C
    
    VarSet
  - Clang_AST
  - Clang_dump
  - Clang_parser
  - Clang_parser_cache
  - Clang_to_C
  - Clang_utils
mopsa.mopsa_c_stubs_parser.parsing
- Parsing
  - Ast
  - Cst
  - Lexer
  - Parser
mopsa.mopsa_c_stubs_parser.passes
- Passes
  - Cst_to_ast
  - Preprocessor
  - Scoping
    
    Scope
mopsa.mopsa_py_parser
- Mopsa_py_parser
  - Ast
    
    VarMap
    
    VarSet
    
    VarSetMap
  - Builtins
  - Cst
  - Cst_to_ast
  - Lexer
  - Main
  - Parser
  - Pp
  - Scoping
mopsa.mopsa_universal_parser
- Mopsa_universal_parser
mopsa.mopsa_utils
- Mopsa_utils
mopsa.mopsa_utils.bitfields
- Bitfields
  - IntBitfields
mopsa.mopsa_utils.congUtils
- CongUtils
  - IntCong
mopsa.mopsa_utils.containers
- Containers
  - Equiv
    
    Make
    
    L
    
    LR
    
    R
    
    RL
    
    OrderedType
  - Graph
    
    IdGeneric
    
    T
    
    IdInt
    
    IdPair
    
    A
    
    B
    
    IdString
    
    IdUnit
    
    Make
    
    EdgeMap
    
    EdgeSet
    
    NodeMap
    
    NodeSet
    
    P
    
    EdgeId
    
    NodeId
    
    Port
  - GraphSig
    
    ID_TYPE
    
    P
    
    EdgeId
    
    NodeId
    
    Port
    
    S
    
    EdgeMap
    
    EdgeSet
    
    NodeMap
    
    NodeSet
    
    P
    
    EdgeId
    
    NodeId
    
    Port
  - InvRelation
    
    Make
    
    CoDom
    
    Dom
  - InvRelationSig
    
    S
    
    CoDomSet
    
    DomSet
  - ListExt
  - MapExt
    
    Int32Map
    
    Int64Map
    
    IntMap
    
    Make
    
    Ord
    
    StringMap
    
    ZMap
  - MapExtPoly
  - MapExtSig
    
    OrderedType
    
    S
  - MapP
    
    Make
    
    E
    
    K
  - Relation
    
    Make
    
    CoDom
    
    Dom
  - RelationSig
    
    S
    
    CoDomSet
  - SetExt
    
    Int32Set
    
    Int64Set
    
    IntSet
    
    Make
    
    Ord
    
    StringSet
    
    ZSet
  - SetExtPoly
  - SetExtSig
    
    S
  - SetP
    
    Make
    
    K
mopsa.mopsa_utils.core
- Utils_core
  - ArgExt
  - Bot
  - Bot_top
  - Callstack
  - Compare
  - Debug
  - Dnf
  - Eq
  - Exceptions
  - LineEdit
    
    FIFO
    
    UBuf
  - Location
  - OptionExt
  - Timing
  - Top
  - TypeExt
  - ValueSig
    
    S
  - Version
mopsa.mopsa_utils.itvUtils
- ItvUtils
  - Float
    
    Double
    
    Single
  - FloatItv
    
    Double
    
    Single
  - FloatItvNan
  - IntBound
  - IntItv

Legend:
Library
Module
Module type
Parameter
Class
Class type

Header of the abstraction

*****************************

type t

Type of the abstract value.

val id : t Core.All.id

Identifier of the value domain

val accept_type : Core.All.typ -> bool

Predicate of types abstracted by the value domain

val name : string

Name of the value domain

val display : string

Display name used in debug messages

val bottom : t

Least abstract element of the lattice.

val top : t

Greatest abstract element of the lattice.

Lattice operators

*********************

val is_bottom : t -> bool

is_bottom a tests whether a is bottom or not.

val subset : t -> t -> bool

Partial order relation. subset a1 a2 tests whether a1 is related to (or included in) a2.

val join : t -> t -> t

join a1 a2 computes an upper bound of a1 and a2.

val meet : t -> t -> t

meet a1 a2 computes a lower bound of a1 and a2.

val widen : 'a Core.All.ctx -> t -> t -> t

widen ctx a1 a2 computes an upper bound of a1 and a2 that ensures stabilization of ascending chains.

Forward semantics

*********************

val constant : Core.All.constant -> Core.All.typ -> t

Evaluation of constants

val unop : Core.All.operator -> Core.All.typ -> t -> Core.All.typ -> t

Evaluation of unary operators

val binop : 
  Core.All.operator ->
  Core.All.typ ->
  t ->
  Core.All.typ ->
  t ->
  Core.All.typ ->
  t

Evaluation of binary operators

val filter : bool -> Core.All.typ -> t -> t

Filter of truth values

val avalue : 'r Core.All.avalue_kind -> t -> 'r option

Cast to avalues

Backward semantics

**********************

val backward_unop : 
  Core.All.operator ->
  Core.All.typ ->
  t ->
  Core.All.typ ->
  t ->
  t

Backward evaluation of unary operators

val backward_binop : 
  Core.All.operator ->
  Core.All.typ ->
  t ->
  Core.All.typ ->
  t ->
  Core.All.typ ->
  t ->
  t * t

Backward evaluation of binary operators

val compare : 
  Core.All.operator ->
  bool ->
  Core.All.typ ->
  t ->
  Core.All.typ ->
  t ->
  t * t

Backward evaluation of comparisons

Pretty printer

******************

val print : Core.All.printer -> t -> unit

Printer of an abstract element.