package codex

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package codex

The Codex static analysis library
- Quick start: verifying C code using Frama-C/Codex
- Tutorials
- Spatial Memory Safety with Dependent Types in Codex
- Extending Codex to a simple while language
- Overview: The While Language
- Lattices and Single Value Abstractions
- Interval Analysis on While Language
- Interval Analysis using Codex
- Library Type_parser
  - Type_parser
- Library codex
  - Codex
    
    Operator
    
    Fixpoint
    
    Codex_config
    
    Codex_log
    
    Hook
    
    Types
    
    Lattices
    
    Single_value_abstraction
    
    Utils
    
    Interval_map
    
    Datatype_sig
    
    Ext
    
    Framac_ival
    
    Domains
    
    Extstdlib
    
    Gui
- Library codex.bdd
  - Bdd
    
    Make
    
    BDD
    
    WithCache
    
    Terminal
    
    MTBDD
    
    Terminal
    
    MTBDD_Make
    
    With_Set
- Library codex.binarytrace
  - Binarytrace
    
    S
    
    To_file
    
    In_Memory
- Library codex.cfg
  - Cfg
    
    Make
    
    Control_location
    
    Node
    
    Control_location
- Library codex.codex_config
  - Codex_config
    
    Log
- Library codex.codex_log
  - Codex_log
    
    S
    
    Default
    
    Null
    
    Dynamic
    
    Tracelog_Instance
    
    Tracelog_Log
    
    Used
- Library codex.compressor
  - Compressor
- Library codex.condition_map
  - Condition_map
    
    L
    
    CONDITION
    
    LConditionMap
    
    L
    
    Cond
    
    LConditionMapFold
    
    L
    
    Cond
    
    ConditionMapTree
    
    Make
    
    L
    
    Cond
    
    ConditionMapPartition
    
    Make
    
    L
    
    Cond
    
    TRANSFER_FUNCTIONS
    
    Cond
    
    MakePathInsensitive
    
    Cond
- Library codex.datatype_sig
  - Datatype_sig
    
    S
    
    Undefined
    
    Conv
    
    Prod2
    
    Prod3
    
    Sum2
    
    Sum3
    
    Int
    
    Unit
    
    String
    
    Option
    
    List
    
    Set
    
    Map
    
    With_Value
    
    Hashtbl
    
    With_Value
    
    StringMap
    
    With_Value
    
    StringHash
    
    With_Value
- Library codex.domains
  - Domains
    
    Assert_false_domain
    
    Dummy_Enum_Lattice
    
    Boolean
    
    Boolean_Backward
    
    Boolean_Forward
    
    Integer
    
    Integer_Forward
    
    Binary
    
    Binary_Forward
    
    Binary_Backward
    
    Enum
    
    Enum_Forward
    
    Domain
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Bitwise
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Extend
    
    Make
    
    MakeForAADT
    
    Integer2binary
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Integer
    
    Integer_Forward
    
    Integer_Query
    
    Log
    
    In_bits
    
    Make_Conversion
    
    Arity
    
    Log_Domain
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Log_With_Focusing
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    Loop_domain
    
    Log
    
    TC
    
    In_bits
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Memory_domains
    
    Assert_false
    
    Block
    
    Block
    
    Block_Forward
    
    Block_Backward
    
    Memory
    
    Memory
    
    Memory_Forward
    
    Memory_Backward
    
    Domain
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Types
    
    Parse_ctypes
    
    Type_check_tree
    
    TypedC
    
    Parse_ctypes
    
    Type_check_tree
    
    TypedC
    
    Block_Forward
    
    Memory_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_smashing
    
    Make
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Convert
    
    Convert_Memory_Forward
    
    C
    
    From_Arity
    
    To_Arity
    
    F
    
    Context
    
    Memory_Forward
    
    Convert_to_monadic
    
    Conversion
    
    From_Arity
    
    To_Arity
    
    Boolean_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Types
    
    Block_Forward
    
    Memory_Forward
    
    Flexible_array_member
    
    Make
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Value
    
    MakeComplete
    
    Scalar
    
    Offset
    
    Scalar
    
    Offset
    
    Value
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Fully_expanded_finite_region
    
    Enumerable_offset
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    Make_Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Memory_domain
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    Region_numeric_offset
    
    Make
    
    Offset
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Scalar
    
    Make_Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Region_separation
    
    Make
    
    Scalar
    
    Offset
    
    Address
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Make_Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Region_suffix_tree
    
    MakeOffset
    
    Scalar
    
    Offset
    
    MakeFullyExpanded
    
    Offset
    
    Scalar
    
    Offset
    
    Scalar
    
    Make_Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Make
    
    Offset
    
    Scalar
    
    Offset
    
    Make_Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Scalar
    
    Symbolic_boolean
    
    AbstractBoolean
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Typed_address
    
    TypedC
    
    MakeAddressOnly
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Query
    
    Binary_Lattice
    
    Make
    
    Scalar
    
    Offset
    
    Address
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Query
    
    Binary_Lattice
    
    Make_Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Value_union_concatenation
    
    MakeAddressOnly
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Make
    
    Scalar
    
    Offset
    
    Address
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Make_Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Wholify
    
    MakeAddressOnly
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Make
    
    Scalar
    
    Offset
    
    Address
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Make_Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    With_focusing
    
    TypedC
    
    BASE_WITH_TYPES
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    S
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    S_with_types
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    Make_with_types
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    Memory_sig
    
    AADT
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    WITH_BOOLEAN_REDEFINITION
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    AADT_WITH_BOOLEAN
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    VALUE
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary_Forward
    
    WITH_OFFSET
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    OFFSET
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    WITH_ADDRESS
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Binary
    
    Query
    
    Binary_Lattice
    
    ADDRESS
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Query
    
    Binary_Lattice
    
    WITH_MEMORY_QUERIES
    
    Context
    
    WITH_FIXED_SIZE_VALUE
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    FIXED_SIZE_VALUE_DOMAIN
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    BLOCK
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Value
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary_Forward
    
    MEMORY
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Address
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Query
    
    Binary_Lattice
    
    Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Value
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary_Forward
    
    OFFSET_AND_MAKE_BLOCK
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Make_Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    ADDRESS_AND_MAKE_MEMORY
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Address
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Query
    
    Binary_Lattice
    
    Make_Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    WHOLE_MEMORY_DOMAIN
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Address
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Make_Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    COMPLETE_DOMAIN
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Offset
    
    Scalar
    
    Offset
    
    Value
    
    Scalar
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Block
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Offset
    
    Value
    
    Memory
    
    Scalar
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    WITH_BLOCK_FORWARD
    
    Context
    
    Block_Forward
    
    WITH_BLOCK
    
    Context
    
    Block_Forward
    
    WITH_MEMORY_FORWARD
    
    Context
    
    Memory_Forward
    
    WITH_BLOCK_OFFSET
    
    Context
    
    WITH_MEMORY
    
    Context
    
    Memory_Forward
    
    WITH_QUERIES
    
    Context
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Base
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Block_Forward
    
    Memory_Forward
    
    Overflow_checks
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Integer
    
    Integer_Forward
    
    Integer_Query
    
    Integer_Lattice
    
    Product
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Sig
    
    Log
    
    Quadrivalent
    
    Context
    
    Context_Arity_Forward
    
    Monadic_Context
    
    With_Boolean_Forward
    
    Context
    
    Boolean_Forward
    
    With_Integer_Forward
    
    Context
    
    Integer_Forward
    
    With_Binary_Forward
    
    Context
    
    Binary_Forward
    
    With_Enum_Forward
    
    Context
    
    Enum_Forward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Enum_Lattice
    
    Binary_Lattice
    
    Integer_Query
    
    Integer_Lattice
    
    WITH_QUERIES
    
    Context
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    With_Types
    
    Context
    
    With_Partitionning
    
    With_Context
    
    Context
    
    With_Assume
    
    Context
    
    With_Nondet
    
    Context
    
    Widening_Id
    
    With_Fixpoint_Computation
    
    Context
    
    Fresh_id
    
    With_Id
    
    With_Boolean
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    With_Integer
    
    Context
    
    Integer
    
    Integer_Forward
    
    Integer_Query
    
    Integer_Lattice
    
    With_Binary
    
    Context
    
    Binary
    
    Binary_Forward
    
    With_Enum
    
    Context
    
    Enum
    
    Enum_Forward
    
    Minimal_No_Boolean
    
    Context
    
    Minimal
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    BASE
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Ext
    
    Context
    
    BASE_WITH_INTEGER
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Integer
    
    Integer_Forward
    
    Integer_Query
    
    Integer_Lattice
    
    Convert_Contexts
    
    From
    
    To
    
    Make_Convert
    
    From_Arity
    
    To_Arity
    
    Convert_Boolean_Forward
    
    C
    
    From_Arity
    
    To_Arity
    
    F
    
    Context
    
    Boolean_Forward
    
    Convert_Integer_Forward
    
    C
    
    From_Arity
    
    To_Arity
    
    F
    
    Context
    
    Integer_Forward
    
    Convert_Binary_Forward
    
    C
    
    From_Arity
    
    To_Arity
    
    F
    
    Context
    
    Binary_Forward
    
    Convert_Enum_Forward
    
    C
    
    From_Arity
    
    To_Arity
    
    F
    
    Context
    
    Enum_Forward
    
    Convert_to_monadic
    
    Conversion
    
    From_Arity
    
    To_Arity
    
    Types
    
    Boolean_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Term_based
    
    Assert_false
    
    Make
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Nonrelational
    
    Make
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    MakeUF
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Product
    
    Make
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Propagation
    
    Make
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Union_find
    
    MakeAdditive
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    MakeLinearTwoVarEquality
    
    Terms
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Term_based_sig
    
    Domain_S
    
    Terms
    
    Condition
    
    Relation
    
    Id
    
    Any
    
    CFG_Node
    
    SUPER_TERMS
    
    Build
    
    Boolean
    
    Integer
    
    Binary
    
    Enum
    
    Mu_Formal
    
    Tuple
    
    Utils
    
    UnionFind
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    DOMAIN_WITH_UNION
    
    Terms
    
    Condition
    
    Relation
    
    Id
    
    Any
    
    CFG_Node
    
    SUPER_TERMS
    
    Build
    
    Boolean
    
    Integer
    
    Binary
    
    Enum
    
    Mu_Formal
    
    Tuple
    
    Utils
    
    UnionFind
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Term_domain
    
    Make
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Integer
    
    Integer_Forward
    
    Integer_Query
    
    Integer_Lattice
    
    With_Noop
    
    Boolean_Backward
    
    Integer_Backward
    
    Binary_Backward
    
    Memory_Backward
- Library codex.emit_alarm
  - Emit_alarm
- Library codex.extstdlib
  - Extstdlib
    
    Array
    
    List
    
    Option
    
    Stream
    
    Map
    
    S
    
    Make
    
    Set
    
    S
    
    Make
- Library codex.file_to_html
  - File_to_html
- Library codex.fixpoint
  - Fixpoint
    
    Fixpoint_graph
    
    Graph
    
    Vertex
    
    Make
    
    ControlLocation
    
    Fixpoint_wto
    
    AbstractDomain
    
    Graph
    
    ControlLocation
    
    Make
    
    CLMap
    
    BaseMap
    
    WithForeign
    
    WithForeign
    
    Reduce
    
    GRAPHI
    
    V
    
    E
    
    Make
    
    Regex
    
    LETTER
    
    S
    
    Make
    
    Region_analysis
    
    NODE
    
    Dict
    
    Set
    
    Graph
    
    DomTree
    
    Edge_Dict
    
    Make
    
    Region_analysis_sig
    
    NODE
    
    Dict
    
    Set
    
    Graph
    
    DomTree
    
    Edge_Dict
    
    Wto
    
    Make
    
    Wto_iteration
    
    ABSTRACTDOMAIN
    
    ControlLocation
    
    WTOFixpoint
    
    CLMap
    
    BaseMap
    
    WithForeign
    
    WithForeign
    
    Wto_utils
    
    NODE
    
    Make
- Library codex.framac_ival
  - Framac_ival
    
    Abstract_interp
    
    Comp
    
    Int
    
    Set
    
    Bool
    
    Bottom
    
    Type
    
    Make_Datatype
    
    Top
    
    Fc_float
    
    Float_interval
    
    Make
    
    Float_interval_sig
    
    S
    
    Float_sig
    
    S
    
    Floating_point
    
    Fval
    
    F
    
    Integer
    
    Ival
    
    Widen_Hints
    
    Ival_noinf
    
    Widen_Hints
    
    Pretty_utils
- Library codex.gui
  - Gui
    
    Interface
    
    Print_html_webapp
- Library codex.hashing
  - Hashing
- Library codex.het-hashtbl
  - HetHashtbl
    
    HETEROGENEOUS_HASHED_TYPE
    
    HETEROGENEOUS_SEEDED_HASHED_TYPE
    
    S
    
    MakeSeeded
    
    Make
- Library codex.hook
  - Hook
- Library codex.int_builtins
  - Int_builtins
- Library codex.interval_map
  - Interval_map
    
    With_Extract
- Library codex.lattices
  - Lattices
    
    Sig
    
    JOIN_SEMI_LATTICE
    
    WITH_INTER
    
    WITH_BOTTOM
    
    WITH_TOP
    
    JOIN_SEMI_LATTICE_WITH_BOTTOM
    
    JOIN_SEMI_LATTICE_WITH_INTER_BOTTOM
    
    LATTICE
    
    BOOLEAN_LATTICE
    
    INTEGER_LATTICE
    
    BITVECTOR_STANDARD_CONVERSIONS
    
    BITVECTOR_LATTICE_NO_CONVERSION
    
    BITVECTOR_QUERIES
    
    BITVECTOR_LATTICE
    
    ENUM_LATTICE
    
    Unimplemented
    
    Enum_Lattice
    
    Bitvector_Lattice
    
    Integer_Lattice
    
    Quadrivalent
    
    Unit
    
    Prod
    
    Prod2
    
    Prod2_With_Bottom
    
    Prod2_With_Inter_Bottom
    
    Known_Bits
    
    BVSet
    
    ZSet
    
    Congruence
    
    Signed_Interval
    
    Unsigned_Interval
    
    Integer
    
    Known_Bits
    
    Bitfield
    
    Bitvector_Of_Integer
    
    Make
- Library codex.online_nearest_common_ancestor_skiplist
  - Online_nearest_common_ancestor_skiplist
    
    Make
- Library codex.operator
  - Operator
    
    Malloc_id
    
    MakeId
    
    Condition
    
    Choice
    
    Alarm
    
    Flags
    
    Bimul
    
    Bshl
    
    Biadd
    
    Bisub
    
    Sig
    
    ARITY
    
    Forward_Arity
    
    Backward_Arity
    
    BOOLEAN_BACKWARD
    
    Arity
    
    BOOLEAN_FORWARD
    
    Arity
    
    INTEGER_BACKWARD
    
    Arity
    
    INTEGER_FORWARD_MIN
    
    Arity
    
    INTEGER_FORWARD
    
    Arity
    
    BITVECTOR_BACKWARD
    
    Arity
    
    BITVECTOR_FORWARD
    
    Arity
    
    BITVECTOR_FORWARD_WITH_BIMUL_ADD
    
    Arity
    
    BINARY_BACKWARD
    
    Arity
    
    BINARY_FORWARD
    
    Arity
    
    OFFSET_BACKWARD
    
    Arity
    
    OFFSET_FORWARD
    
    Arity
    
    BLOCK_BACKWARD
    
    Arity
    
    BLOCK_FORWARD
    
    Arity
    
    ENUM_BACKWARD
    
    Arity
    
    ENUM_FORWARD
    
    Arity
    
    MEMORY_BACKWARD
    
    Arity
    
    MEMORY_FORWARD
    
    Arity
    
    ARITY
    
    Forward_Arity
    
    Backward_Arity
    
    BOOLEAN_BACKWARD
    
    BOOLEAN_FORWARD
    
    INTEGER_BACKWARD
    
    INTEGER_FORWARD_MIN
    
    INTEGER_FORWARD
    
    BITVECTOR_BACKWARD
    
    BITVECTOR_FORWARD
    
    BITVECTOR_FORWARD_WITH_BIMUL_ADD
    
    BINARY_BACKWARD
    
    BINARY_FORWARD
    
    OFFSET_BACKWARD
    
    OFFSET_FORWARD
    
    BLOCK_BACKWARD
    
    BLOCK_FORWARD
    
    ENUM_BACKWARD
    
    ENUM_FORWARD
    
    MEMORY_BACKWARD
    
    MEMORY_FORWARD
    
    Concrete
    
    In_bits
    
    Types
    
    Boolean_Interp
    
    Bitvector_Interp
    
    Function_symbol
    
    Build
    
    Arity
    
    Binary
    
    PRETTY_ARG
    
    PRETTY_RESULT
    
    Pretty
    
    Conversions
    
    Conversion
    
    From_Arity
    
    To_Arity
    
    Convert_Boolean_Forward
    
    Convert_Integer_Forward
    
    Convert_Bitvector_Forward
    
    Convert_Binary_Forward
    
    Convert_Block_Forward
    
    Convert_Enum_Forward
    
    Convert_Memory_Forward
    
    Autolog
    
    BOOLEAN_CONVERSION
    
    Arity
    
    INTEGER_CONVERSION
    
    Arity
    
    ENUM_CONVERSION
    
    Arity
    
    BITVECTOR_CONVERSION
    
    Arity
    
    MEMORY_CONVERSION
    
    Arity
    
    Log_Boolean_Backward
    
    Log_Integer_Backward
    
    Log_Bitvector_Forward
    
    Log_Bitvector_Forward_With_Bimul_add
    
    Log_Binary_Forward
    
    Log_Enum_Forward
    
    Log_Memory_Forward
- Library codex.record_time
  - Record_time
- Library codex.single_value_abstraction
  - Single_value_abstraction
    
    Sig
    
    Quadrivalent
    
    Bitfield
    
    WITH_BOOLEAN_FORWARD
    
    Boolean_Forward
    
    WITH_INTEGER_FORWARD
    
    Integer_Forward
    
    WITH_BITVECTOR_FORWARD
    
    Bitvector_Forward
    
    WITH_ENUM_FORWARD
    
    Enum_Forward
    
    WITH_BLOCK_FORWARD
    
    Block_Forward
    
    WITH_MEMORY_FORWARD
    
    Memory_Forward
    
    WITH_MEMORY_BITVECTOR_BOOLEAN_FORWARD
    
    Memory_Forward
    
    Block_Forward
    
    Bitvector_Forward
    
    Boolean_Forward
    
    WITH_MEMORY_BITVECTOR_INTEGER_BOOLEAN_FORWARD
    
    Memory_Forward
    
    Block_Forward
    
    Bitvector_Forward
    
    Integer_Forward
    
    Boolean_Forward
    
    WITH_FORWARD
    
    Memory_Forward
    
    Block_Forward
    
    Bitvector_Forward
    
    Integer_Forward
    
    Boolean_Forward
    
    WITH_BOOLEAN_BACKWARD
    
    Boolean_Backward
    
    WITH_INTEGER_BACKWARD
    
    Integer_Backward
    
    WITH_ENUM_BACKWARD
    
    Enum_Backward
    
    WITH_BITVECTOR_BACKWARD
    
    Bitvector_Backward
    
    WITH_BLOCK_BACKWARD
    
    Block_Backward
    
    WITH_MEMORY_BACKWARD
    
    Memory_Backward
    
    WITH_MEMORY_BITVECTOR_BOOLEAN_BACKWARD
    
    Memory_Backward
    
    Block_Backward
    
    Bitvector_Backward
    
    Boolean_Backward
    
    WITH_BOOLEAN_FORWARD_BACKWARD
    
    Boolean_Forward
    
    Boolean_Backward
    
    WITH_INTEGER_FORWARD_BACKWARD
    
    Integer_Forward
    
    Integer_Backward
    
    WITH_ENUM_FORWARD_BACKWARD
    
    Enum_Forward
    
    Enum_Backward
    
    WITH_BITVECTOR_FORWARD_BACKWARD
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    WITH_BLOCK_FORWARD_BACKWARD
    
    Block_Forward
    
    Block_Backward
    
    WITH_MEMORY_FORWARD_BACKWARD
    
    Memory_Forward
    
    Memory_Backward
    
    WITH_BITVECTOR_BOOLEAN_FORWARD_BACKWARD
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    WITH_MEMORY_BITVECTOR_BOOLEAN_FORWARD_BACKWARD
    
    Memory_Forward
    
    Memory_Backward
    
    Block_Forward
    
    Block_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    WITH_FORWARD_BACKWARD
    
    Memory_Forward
    
    Memory_Backward
    
    Block_Forward
    
    Block_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    BOOLEAN_LATTICE
    
    INTEGER_LATTICE
    
    BITVECTOR_LATTICE
    
    ENUM_LATTICE
    
    MEMORY_LATTICE
    
    BLOCK_LATTICE
    
    BOOLEAN
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    INTEGER
    
    Integer_Forward
    
    Integer_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    ENUM
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Enum_Lattice
    
    BITVECTOR
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    BITVECTOR_ENUM
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    NUMERIC
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    NUMERIC_ENUM
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    ALL
    
    Boolean_Forward
    
    Boolean_Backward
    
    Integer_Forward
    
    Integer_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Block_Forward
    
    Block_Backward
    
    Memory_Forward
    
    Memory_Backward
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Lattice
    
    Memory_Lattice
    
    Enum_Lattice
    
    Block_Lattice
    
    Quadrivalent
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Ival
    
    Integer_Forward
    
    Integer_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Bitvector_Lattice
    
    Bitfield
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    Known_bits
    
    Dummy
    
    Make
    
    Dummy_Enum_Lattice
    
    Dummy_Integer_Lattice
    
    Complete_Binary
    
    Boolean_Forward
    
    Boolean_Backward
    
    Integer_Forward
    
    Integer_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Block_Forward
    
    Block_Backward
    
    Memory_Forward
    
    Memory_Backward
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Lattice
    
    Memory_Lattice
    
    Enum_Lattice
    
    Block_Lattice
    
    Complete_Bitvector_Enum
    
    Boolean_Forward
    
    Boolean_Backward
    
    Integer_Forward
    
    Integer_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Block_Forward
    
    Block_Backward
    
    Memory_Forward
    
    Memory_Backward
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Lattice
    
    Memory_Lattice
    
    Enum_Lattice
    
    Block_Lattice
    
    Complete_Integer
    
    Boolean_Forward
    
    Boolean_Backward
    
    Integer_Forward
    
    Integer_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Block_Forward
    
    Block_Backward
    
    Memory_Forward
    
    Memory_Backward
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Lattice
    
    Memory_Lattice
    
    Enum_Lattice
    
    Block_Lattice
    
    Dummy_All
    
    Boolean_Forward
    
    Boolean_Backward
    
    Integer_Forward
    
    Integer_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Block_Forward
    
    Block_Backward
    
    Memory_Forward
    
    Memory_Backward
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Lattice
    
    Memory_Lattice
    
    Enum_Lattice
    
    Block_Lattice
    
    Log
    
    Sig
    
    Quadrivalent
    
    Bitfield
    
    WITH_BOOLEAN_FORWARD
    
    Boolean_Forward
    
    WITH_INTEGER_FORWARD
    
    Integer_Forward
    
    WITH_BITVECTOR_FORWARD
    
    Bitvector_Forward
    
    WITH_ENUM_FORWARD
    
    Enum_Forward
    
    WITH_BLOCK_FORWARD
    
    Block_Forward
    
    WITH_MEMORY_FORWARD
    
    Memory_Forward
    
    WITH_MEMORY_BITVECTOR_BOOLEAN_FORWARD
    
    Memory_Forward
    
    Block_Forward
    
    Bitvector_Forward
    
    Boolean_Forward
    
    WITH_MEMORY_BITVECTOR_INTEGER_BOOLEAN_FORWARD
    
    Memory_Forward
    
    Block_Forward
    
    Bitvector_Forward
    
    Integer_Forward
    
    Boolean_Forward
    
    WITH_FORWARD
    
    Memory_Forward
    
    Block_Forward
    
    Bitvector_Forward
    
    Integer_Forward
    
    Boolean_Forward
    
    WITH_BOOLEAN_BACKWARD
    
    Boolean_Backward
    
    WITH_INTEGER_BACKWARD
    
    Integer_Backward
    
    WITH_ENUM_BACKWARD
    
    Enum_Backward
    
    WITH_BITVECTOR_BACKWARD
    
    Bitvector_Backward
    
    WITH_BLOCK_BACKWARD
    
    Block_Backward
    
    WITH_MEMORY_BACKWARD
    
    Memory_Backward
    
    WITH_MEMORY_BITVECTOR_BOOLEAN_BACKWARD
    
    Memory_Backward
    
    Block_Backward
    
    Bitvector_Backward
    
    Boolean_Backward
    
    WITH_BOOLEAN_FORWARD_BACKWARD
    
    Boolean_Forward
    
    Boolean_Backward
    
    WITH_INTEGER_FORWARD_BACKWARD
    
    Integer_Forward
    
    Integer_Backward
    
    WITH_ENUM_FORWARD_BACKWARD
    
    Enum_Forward
    
    Enum_Backward
    
    WITH_BITVECTOR_FORWARD_BACKWARD
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    WITH_BLOCK_FORWARD_BACKWARD
    
    Block_Forward
    
    Block_Backward
    
    WITH_MEMORY_FORWARD_BACKWARD
    
    Memory_Forward
    
    Memory_Backward
    
    WITH_BITVECTOR_BOOLEAN_FORWARD_BACKWARD
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    WITH_MEMORY_BITVECTOR_BOOLEAN_FORWARD_BACKWARD
    
    Memory_Forward
    
    Memory_Backward
    
    Block_Forward
    
    Block_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    WITH_FORWARD_BACKWARD
    
    Memory_Forward
    
    Memory_Backward
    
    Block_Forward
    
    Block_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    BOOLEAN_LATTICE
    
    INTEGER_LATTICE
    
    BITVECTOR_LATTICE
    
    ENUM_LATTICE
    
    MEMORY_LATTICE
    
    BLOCK_LATTICE
    
    BOOLEAN
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    INTEGER
    
    Integer_Forward
    
    Integer_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    ENUM
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Enum_Lattice
    
    BITVECTOR
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    BITVECTOR_ENUM
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    NUMERIC
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    NUMERIC_ENUM
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    ALL
    
    Boolean_Forward
    
    Boolean_Backward
    
    Integer_Forward
    
    Integer_Backward
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Block_Forward
    
    Block_Backward
    
    Memory_Forward
    
    Memory_Backward
    
    Enum_Forward
    
    Enum_Backward
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Bitvector_Lattice
    
    Memory_Lattice
    
    Enum_Lattice
    
    Block_Lattice
    
    Log_Numeric_Enum
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    No_Log_Numeric_Enum
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    Stats
    
    In_bits
    
    IntMap
    
    Log
    
    Make
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
- Library codex.smallmap
  - Smallmap
    
    Make
- Library codex.smtbackend
  - Smtbackend
    
    Smtlib_sig
    
    COMMON_S
    
    TYPED_S
    
    UNTYPED_S
    
    UNTYPED_MUZ
    
    PARAM_S
    
    Smtlib
    
    COMMON_S
    
    TYPED_S
    
    UNTYPED_S
    
    UNTYPED_MUZ
    
    PARAM_S
    
    Make_Typed
    
    Make_Untyped
    
    Make_Untyped_Muz
- Library codex.stats
  - Stats
    
    StatLogger
- Library codex.syntax_tree
  - Syntax_tree
    
    Location_identifier
- Library codex.terms
  - Terms
    
    Builder
    
    Make
    
    Condition
    
    Relation
    
    Id
    
    Any
    
    CFG_Node
    
    SUPER_TERMS
    
    Build
    
    Boolean
    
    Integer
    
    Binary
    
    Enum
    
    Mu_Formal
    
    Tuple
    
    Utils
    
    UnionFind
    
    Condition
    
    Bed
    
    BDD
    
    WithCache
    
    Terminal
    
    MTBDD
    
    Terminal
    
    MTBDD_Make
    
    With_Set
    
    ConditionMy
    
    WithCache
    
    ConditionDom
    
    Literal
    
    Path
    
    AppendHash
    
    JoinHash
    
    Log
    
    ConditionInt
    
    ConditionCudd
    
    C_bdd
    
    MakeConditionCudd
    
    MakeConditionMapMTBDD
    
    Maybe_Lattice
    
    MTBDD
    
    Terminal
    
    With_Set
    
    L
    
    Cond
    
    SCONDITIONMAP_MTBDD
    
    L
    
    Cond
    
    MTBDD
    
    Terminal
    
    ConditionMapMTBDD
    
    Cond
    
    MakeConditionMapPartitionPI
    
    ConditionMapPartition
    
    Make
    
    L
    
    Cond
    
    SCONDITIONMAP
    
    L
    
    Cond
    
    MakeConditionMap
    
    L
    
    Cond
    
    ConditionMap
    
    PI
    
    Cond
    
    Cond
    
    MakeConditionMapTreePI
    
    ConditionMapTree
    
    Make
    
    L
    
    Cond
    
    MakeConditionMap
    
    L
    
    Cond
    
    ConditionMap
    
    PI
    
    Cond
    
    Cond
    
    CuddMTBDD
    
    SCONDITIONMAP_CUDD_MTBDD
    
    L
    
    Cond
    
    MakeConditionMapCuddMTBDD
    
    TerminalHash
    
    IfHash
    
    Cond
    
    L
    
    T
    
    Find_cache
    
    Find_all_cache
    
    Refine_cache
    
    Loop_cache
    
    T2_cache
    
    Value_cache
    
    CuddTree
    
    SCONDITIONMAP_CUDD_TREE
    
    L
    
    Cond
    
    MakeConditionMapCuddTree
    
    TerminalHash
    
    IfHash
    
    Cond
    
    L
    
    CuddPIPartition
    
    Condition
    
    ConditionMapPartition
    
    Make
    
    L
    
    Cond
    
    SCONDITIONMAP
    
    L
    
    Cond
    
    MakeConditionMap
    
    L
    
    Cond
    
    ConditionMap
    
    PI
    
    Cond
    
    Cond
    
    DomPIPartition
    
    Condition
    
    M
    
    SCONDITIONMAP
    
    ConditionMap
    
    MakeConditionMap
    
    CuddPITree
    
    Condition
    
    ConditionMap
    
    Cond
    
    MakeConditionMap
    
    SCONDITIONMAP
    
    CuddPIMTBDD
    
    Condition
    
    ConditionMap
    
    Cond
    
    MakeConditionMap
    
    SCONDITIONMAP
    
    HomeMadeBDDPartitionPI
    
    Condition
    
    ConditionMapPartition
    
    Make
    
    L
    
    Cond
    
    SCONDITIONMAP
    
    L
    
    Cond
    
    MakeConditionMap
    
    L
    
    Cond
    
    ConditionMap
    
    PI
    
    Cond
    
    Cond
    
    HomeMadeMTBDD
    
    Condition
    
    MakeConditionMap
    
    SCONDITIONMAP
    
    ConditionMap
    
    Const_eval
    
    Make
    
    Relations
    
    GROUP_ACTION
    
    Equality
    
    Action
    
    Additive
    
    Action
    
    XOR_Rotate
    
    LinearTwoVarEquality
    
    Action
    
    Sig
    
    TERMS
    
    Condition
    
    Relation
    
    Id
    
    Any
    
    CFG_Node
    
    SUPER_TERMS
    
    Build
    
    Boolean
    
    Integer
    
    Binary
    
    Enum
    
    Mu_Formal
    
    Tuple
    
    Utils
    
    UnionFind
    
    Slicing
    
    Make
    
    Smt
    
    MakeFirstOrder
    
    MakeHorn
- Library codex.tracelog
  - Tracelog
    
    S
    
    Make
    
    MakeDebug
    
    MakeSilent
    
    Dummy
- Library codex.treemap
  - Treemap
    
    Key
    
    Make_no_empty
    
    Make
- Library codex.types
  - Types
    
    Parse_ctypes
    
    Type_check_tree
    
    TypedC
    
    Pred
    
    Constr
    
    Build
- Library codex.union_find
  - Union_Find
    
    Functional
    
    GenericRelationalValued
    
    EltSet
    
    BaseMap
    
    WithForeign
    
    Imperative
    
    MakeNode
    
    Relation
    
    MakeNumberedNode
    
    Relation
    
    MakeValuedNode
    
    Relation
    
    Value
    
    MakeValuedNumberedNode
    
    Relation
    
    Value
    
    HashtblSimpleNode
    
    Relation
    
    GenericRelationalValued
    
    GenericRelational
    
    Parameters
    
    SIMPLE_GENERIC_ELT
    
    GENERIC_ELT
    
    GENERIC_MONOID
    
    GENERIC_GROUP
    
    SIMPLE_GENERIC_VALUE
    
    GENERIC_VALUE
    
    UF_NODE
    
    Relation
    
    UF_NODE_WITH_VALUE
    
    Relation
    
    Value
    
    Signatures
    
    IMPERATIVE_GENERIC_RELATIONAL
    
    IMPERATIVE_GENERIC_RELATIONAL_VALUED
- Library codex.units
  - Units
    
    Unit
    
    In_bits
    
    In_bytes
- Library codex.while_ast
  - While_ast
    
    Var
- Library codex.whilelib
  - Whilelib
    
    Analysis_sva
    
    Var
    
    Log
    
    SVA_Ival
    
    SVA_Bval
    
    State
    
    BaseMap
    
    WithForeign
    
    WithForeign
    
    Cinterpreter
    
    State
    
    While_analysis
    
    Log
    
    Terms
    
    Condition
    
    Relation
    
    Id
    
    Any
    
    CFG_Node
    
    SUPER_TERMS
    
    Build
    
    Boolean
    
    Integer
    
    Binary
    
    Enum
    
    Mu_Formal
    
    Tuple
    
    Utils
    
    UnionFind
    
    SVA
    
    Bitvector_Forward
    
    Bitvector_Backward
    
    Boolean_Forward
    
    Boolean_Backward
    
    Boolean_Lattice
    
    Bitvector_Lattice
    
    Integer_Forward
    
    Integer_Backward
    
    Integer_Lattice
    
    Enum_Forward
    
    Enum_Backward
    
    Enum_Lattice
    
    NonRelationalDomain
    
    Terms
    
    Condition
    
    Relation
    
    Id
    
    Any
    
    CFG_Node
    
    SUPER_TERMS
    
    Build
    
    Boolean
    
    Integer
    
    Binary
    
    Enum
    
    Mu_Formal
    
    Tuple
    
    Utils
    
    UnionFind
    
    Integer_Query
    
    Integer_Lattice
    
    Query
    
    Boolean_Lattice
    
    Integer_Lattice
    
    Binary_Lattice
    
    Enum_Lattice
    
    Domain_Arity
    
    Boolean_Forward
    
    Integer_Forward
    
    Binary_Forward
    
    Enum_Forward
    
    Domain
    
    Context
    
    Boolean
    
    Boolean_Forward
    
    Query
    
    Binary_Lattice
    
    Enum_Lattice
    
    Binary
    
    Binary_Forward
    
    Enum
    
    Enum_Forward
    
    Integer
    
    Integer_Forward
    
    Integer_Query
    
    Integer_Lattice
    
    Var
    
    Store
    
    While_examples
- Library immutable_array
  - Immutable_array
- Library interface
  - Interface
    
    Int64Map
    
    Graph
    
    Wto
- Library ppx_while
  - Ppx_while
- Library type_parse_tree
  - Type_parse_tree
    
    Symbol
    
    Pretty
- Sources
  - Type_parser
    
    type_parser.ml
  - codex
    
    codex.ml
  - codex.bdd
    
    bdd.ml
  - codex.binarytrace
    
    binarytrace.ml
  - codex.cfg
    
    cfg.ml
    
    cfg__.ml
  - codex.codex_config
    
    codex_config.ml
  - codex.codex_log
    
    codex_log.ml
  - codex.compressor
    
    compressor.ml
  - codex.condition_map
    
    condition_map.ml
  - codex.datatype_sig
    
    datatype_sig.ml
  - codex.domains
    
    assert_false_domain.ml
    
    bitwise.ml
    
    domains.ml
    
    extend.ml
    
    integer2binary.ml
    
    log.ml
    
    loop_domain.ml
    
    overflow_checks.ml
    
    product.ml
    
    sig.ml
    
    term_domain.ml
    
    with_Noop.ml
  - codex.emit_alarm
    
    emit_alarm.ml
  - codex.extstdlib
    
    extstdlib.ml
  - codex.file_to_html
    
    file_to_html.ml
  - codex.fixpoint
    
    fixpoint.ml
    
    fixpoint_graph.ml
    
    fixpoint_wto.ml
    
    reduce.ml
    
    regex.ml
    
    region_analysis.ml
    
    region_analysis_sig.ml
    
    wto.ml
    
    wto_iteration.ml
    
    wto_utils.ml
  - codex.framac_ival
    
    abstract_interp.ml
    
    bottom.ml
    
    fc_float.ml
    
    float_interval.ml
    
    floating_point.ml
    
    framac_ival.ml
    
    fval.ml
    
    integer.ml
    
    ival.ml
    
    ival_noinf.ml
    
    pretty_utils.ml
  - codex.gui
    
    binsec_webapp_string.ml
    
    bundle_string.ml
    
    graphviz_string.ml
    
    gui.ml
    
    gui__.ml
    
    print_html_webapp.ml
    
    tailwindcss_string.ml
  - codex.hashing
    
    hashing.ml
  - codex.het-hashtbl
    
    hetHashtbl.ml
  - codex.hook
    
    hook.ml
  - codex.int_builtins
    
    int_builtins.ml
  - codex.interval_map
    
    interval_map.ml
  - codex.lattices
    
    bitfield_Lattice.ml
    
    bitvector_Of_Integer.ml
    
    bitvector_standard.ml
    
    boolean_standard.ml
    
    integer_standard.ml
    
    lattices.ml
    
    lattices__.ml
    
    prod_Lattice.ml
    
    quadrivalent_Lattice.ml
    
    set_Lattice.ml
    
    unimplemented_Lattice.ml
    
    unit_Lattice.ml
  - codex.online_nearest_common_ancestor_skiplist
    
    online_nearest_common_ancestor_skiplist.ml
  - codex.operator
    
    flags.ml
    
    function_symbol.ml
    
    operator.ml
    
    operator__.ml
    
    operator_alarm.ml
    
    operator_autolog.ml
    
    operator_concrete.ml
    
    operator_conversions.ml
    
    operator_ids.ml
    
    operator_sig.ml
  - codex.record_time
    
    record_time.ml
  - codex.single_value_abstraction
    
    binary_collecting.ml
    
    binary_test.ml
    
    single_value_abstraction.ml
    
    single_value_abstraction__.ml
    
    sva_Assert_False_Transfer_Functions.ml
    
    sva_binary_to_integer.ml
    
    sva_bitfield.ml
    
    sva_dummy.ml
    
    sva_ival.ml
    
    sva_ival_with_sentinel.ml
    
    sva_known_bits.ml
    
    sva_log.ml
    
    sva_noop_transfer_functions.ml
    
    sva_prod.ml
    
    sva_quadrivalent.ml
    
    sva_reduced_prod.ml
    
    sva_sentinel.ml
    
    sva_sig.ml
    
    sva_stats.ml
  - codex.smallmap
    
    smallmap.ml
  - codex.smtbackend
    
    smtbackend.ml
    
    smtbackend__.ml
    
    smtbackend_aliases.ml
    
    smtbackend_smtlib.ml
    
    smtbackend_smtlib_sig.ml
  - codex.stats
    
    stats.ml
  - codex.syntax_tree
    
    syntax_tree.ml
  - codex.terms
    
    builder.ml
    
    condition.ml
    
    const_eval.ml
    
    relations.ml
    
    slicing.ml
    
    smt.ml
    
    terms.ml
  - codex.tracelog
    
    common.ml
    
    terminal.ml
    
    tracelog.ml
    
    tracelog__.ml
  - codex.treemap
    
    treemap.ml
  - codex.types
    
    parse_ctypes.ml
    
    type_check_tree.ml
    
    typedC.ml
    
    types.ml
  - codex.union_find
    
    functional.ml
    
    imperative.ml
    
    union_Find.ml
  - codex.units
    
    units.ml
  - codex.while_ast
    
    while_ast.ml
  - codex.whilelib
    
    analysis_sva.ml
    
    cinterpreter.ml
    
    while_analysis.ml
    
    while_examples.ml
    
    whilelib.ml
  - immutable_array
    
    immutable_array.ml
  - interface
    
    interface.ml
  - ppx_while
    
    ppx_while.ml
  - type_parse_tree
    
    type_parse_tree.ml

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

Module `Wto_iteration.WTOFixpoint`Source

Parameters

module L : ABSTRACTDOMAIN

Signature

Sourcemodule CLMap : PatriciaTree.MAP with type key = L.ControlLocation.t

Source

val fixpoint_partition : 
  L.t CLMap.t ->
  L.ControlLocation.t Wto.partition ->
  L.t CLMap.t

package codex

Module Wto_iteration.WTOFixpointSource

Parameters

Signature

Module `Wto_iteration.WTOFixpoint`Source