package binsec

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package binsec

binsec
- Binsec
  - Array_utils
  - Ast
    
    Expr
    
    Instr
    
    Loc
    
    Obj
    
    Size
    
    Symbol
  - Ast_types
    
    AST
    
    Expr
    
    Instr
    
    LValue
    
    ENV
    
    PARSER_EXPRESSION
  - Base_logger
  - Basic_types
    
    BigInt
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Collection_make
    
    Auto
    
    C
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Default
    
    C
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Hashed
    
    C
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Constants
    
    Float
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Int
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Int64
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    String
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Ternary
  - Binpatcher
    
    PatchMap
    
    WritableLoader
  - Binpatcher_options
    
    Logger
    
    PatchFile
    
    PatchOutFile
  - Binstream
  - Bitset
  - Bitvector
    
    Collection
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Common
  - Cfg
    
    Make
    
    A
    
    E
    
    Fixpoint
    
    X
    
    V
    
    S
    
    E
    
    Fixpoint
    
    X
    
    V
  - Cfgraph
    
    Dot
    
    G
    
    E
    
    V
  - Cli
    
    BOOLEAN
    
    Boot
    
    CLI_DECL
    
    Cli_sig
    
    Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    Debug_level
    
    Logger
    
    Loglevel
    
    Quiet
    
    DECL
    
    DEFAULTED_CLI_DECL
    
    DETAILED_CLI_DECL
    
    FLOAT
    
    FLOAT_LIST
    
    FLOAT_OPT
    
    FLOAT_SET
    
    GENERIC
    
    GENERIC_OPT
    
    INTEGER
    
    INTEGER_LIST
    
    INTEGER_OPT
    
    INTEGER_SET
    
    Make
    
    Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    D
    
    Debug_level
    
    Logger
    
    Loglevel
    
    Quiet
    
    Options
    
    Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    D
    
    Debug_level
    
    Logger
    
    Loglevel
    
    Quiet
    
    S
    
    Logger
    
    STRING
    
    STRING_LIST
    
    STRING_OPT
    
    STRING_SET
  - Colors
    
    FlatUI
  - Concrete
    
    Dba_program
    
    Env
    
    Image
    
    Instr_list
    
    Interpreter
    
    P
    
    Program
  - Dba
    
    Binary_op
    
    Expr
    
    Instr
    
    Jump_target
    
    LValue
    
    Tag
    
    Unary_op
    
    Var
    
    Tag
  - Dba_printer
    
    Ascii
    
    DbaPrinter
    
    EICAscii
    
    EICUnicode
    
    Make
    
    R
    
    Renderer
    
    Unicode
  - Dba_to_formula
  - Dba_types
    
    AddressStack
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Caddress
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Call_stack
    
    Declarations
    
    Expr
    
    Instruction
    
    Jump_target
    
    LValue
    
    Logger
    
    Statement
    
    Var
    
    Hamt
    
    Htbl
    
    Map
    
    Set
  - Dba_utils
    
    Expr
  - Dba_visitor
    
    dba_inplace_visitor
    
    inplace_visitor_t
  - Dbacsl_parser
  - Dbacsl_token
  - Decode_utils
  - Dhunk
    
    Check
  - Directive
    
    Action
    
    Choice
    
    Count
  - Disasm
    
    Program
    
    Recursive
  - Disasm_cfg
  - Disasm_core
    
    Iterable
    
    Make
    
    I
    
    Successors
    
    W
  - Disasm_options
    
    CFG_graph
    
    Cache_decoder
    
    DbaOutputFile
    
    Decode_instruction
    
    Decode_replacement
    
    Disasm_at
    
    Disassembly_mode
    
    Functions
    
    Logger
    
    NoLoaderMode
    
    OpcodeOutputFile
    
    Sections
    
    ShowInstructionCount
  - Dwarf
  - Dwarf_cunit
    
    Func
    
    Global
    
    Type
    
    Var
  - Dwarf_expr
  - Dwarf_frame
  - Dwarf_lines
  - Dwarf_options
    
    Logger
  - Dwarf_utils
  - Elf_options
    
    Alloc
    
    Logger
    
    Reloc
  - Errors
  - File_utils
  - Formula
    
    Printing
  - Formula_main
  - Formula_options
    
    Flatten_memory
    
    Logger
    
    No_stitching
    
    OptimAll
    
    OptimCst
    
    OptimItv
    
    OptimLst
    
    OptimPrn
    
    OptimRbs
    
    OptimRow
    
    OptimSsa
    
    Solver
    
    Options
    
    Timeout
  - Formula_pp
  - Formula_solver
    
    Command
    
    Session
  - Formula_to_smtlib
  - Formula_transformation
  - Formula_utils
    
    BindEnv
  - Ghidra_cfg
    
    E
    
    V
  - Ghidra_options
    
    Cache
    
    Logger
    
    Runner
  - Hash
  - Hashamt
    
    Make
    
    S
  - Htx_main
  - Htx_options
    
    Directory
    
    Level
    
    Logger
  - Ida
  - Ida_cfg
    
    C
    
    E
    
    Fixpoint
    
    X
    
    V
    
    F
    
    Function
    
    G
    
    S
  - Ida_cg
    
    E
    
    Edge
    
    Fixpoint
    
    X
    
    Node
    
    T
    
    Parse
    
    V
  - Ida_options
    
    IdaCfg
    
    IdaOutputFile
    
    IdaSimpleCfg
    
    Logger
  - Ida_utils
    
    Dot
  - Imap
  - Infos
    
    BoundThreshold
    
    WideningThreshold
  - Instr_cfg
    
    E
    
    Fixpoint
    
    X
    
    Make
    
    E
    
    Fixpoint
    
    X
    
    V
    
    S
    
    E
    
    Fixpoint
    
    X
    
    V
    
    V
  - Instruction
    
    Basic
    
    Generic
    
    Make
    
    P
  - Interval
    
    BitVec
    
    BitVecFlat
    
    Flat
    
    Ord
    
    Float
    
    FloatFlat
    
    Int
    
    IntFlat
    
    Make
    
    Ord
    
    S
  - Isa_helper
  - Kernel_core
  - Kernel_functions
    
    Loader
  - Kernel_options
    
    Config_file
    
    Dba_config
    
    Dba_file
    
    Decoder
    
    Describe_binary
    
    Entry_point
    
    ExecFile
    
    Experimental
    
    Logger
    
    Machine
    
    Version
  - Lexer
  - Lexer_ghidra
  - List_utils
  - Lmap
    
    Make
    
    E
    
    S
    
    Value
  - Loader
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
    
    View
  - Loader_buf
    
    Bufferable
    
    Make
    
    B
    
    Peek
    
    Read
    
    Peek
    
    Read
    
    S
    
    Peek
    
    Read
    
    W
    
    Peek
    
    Read
    
    Write
    
    Wake
    
    Peek
    
    Read
    
    W
    
    Write
    
    Writable
    
    Write
  - Loader_elf
    
    Address
    
    Peek
    
    Read
    
    E_class
    
    E_ident
    
    Ehdr
    
    ET
    
    Img
    
    Note
    
    Offset
    
    Peek
    
    Read
    
    Phdr
    
    Rel
    
    Section
    
    Shdr
    
    SHF
    
    SHN
    
    SHT
    
    Sym
    
    STB
    
    STT
    
    Symbol
    
    Utils
  - Loader_pe
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
  - Loader_raw
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
  - Loader_sigs
    
    S
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
  - Loader_ti83
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
  - Loader_types
  - Loader_utils
    
    Binary_loc
  - Location
  - Logger
    
    ChannelGroup
    
    Make
    
    G
    
    S
  - Lreader
    
    Accessor
    
    Peek
    
    Read
  - Machine
    
    Bitwidth
    
    Endianness
    
    ISA
  - Mcount_main
  - Mcount_options
    
    Limit
    
    Logger
  - Mnemonic
  - Natural
  - Parse_helpers
    
    Declarations
    
    Initialization
    
    Message
    
    Value
    
    Mk
    
    Predicates
  - Parse_utils
  - Parser
  - Parser_ghidra
  - Plugins
    
    Plugins
    
    Sites
  - Predba
  - Prettytbl
    
    Column
  - Print_utils
  - Prover
    
    Command
  - Riscv_arch
    
    Mode
    
    Register
    
    M
    
    RegisterSize
    
    S
  - Riscv_options
    
    Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    Debug_level
    
    Logger
    
    Loglevel
    
    Odump_file
    
    Quiet
  - Riscv_to_dba
  - Runtime
    
    Sites
  - Sequence
  - Sigs
    
    ANY
    
    ARITHMETIC
    
    BITWISE
    
    COMPARABLE
    
    COMPARABLE_EXT
    
    COMPARISON
    
    Collection
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    EXTENDED_LOGICAL
    
    Eq
    
    HASHABLE
    
    HASHABLE_AUTO
    
    ITERABLE
    
    LOGICAL
    
    PRINTABLE
    
    SHIFT_ROT
    
    STRINGIFIABLE
    
    STR_INJECTIBLE
  - Simulation
    
    Directives
    
    InitFile
    
    Logger
    
    MemoryFile
  - Size
    
    Bit
    
    Byte
    
    Size
  - Smt_model
  - Smtlib
  - Smtlib_lexer
  - Smtlib_options
    
    Logger
    
    Model_from_file
  - Smtlib_parser
  - Smtlib_pp
  - Smtlib_to_formula
  - Smtlib_utils
  - String_utils
  - Subprocess
  - Suid
  - Term
    
    Bv
    
    Collection
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Common
    
    Make
    
    A
    
    B
    
    Op
    
    S
  - Utils
  - Virtual_address
    
    Hamt
    
    Htbl
    
    Map
    
    Set
  - Worklist
    
    CMake
    
    X
    
    Make
    
    X
    
    S
  - X86Instruction
  - X86Types
  - X86Util
  - X86_options
    
    HandleSegments
    
    Logger
    
    ProtectedMode
  - X86decoder
  - X86pp
  - X86toDba
  - Z80_arch
  - Z80_options
    
    Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    Debug_level
    
    Logger
    
    Loglevel
    
    Quiet
  - Z80_to_dba
binsec.amd64decoder
- Amd64decoder
  - Amd64ToDba
  - Amd64_options
    
    Logger
binsec.armv7decoder
- Armv7decoder
  - ArmToDba
  - Arm_options
    
    Logger
    
    SupportedModes
binsec.armv8decoder
- Armv8decoder
  - Aarch64ToDba
  - Aarch64_options
    
    Logger
binsec.domains
- Domains
  - Interval
  - S
binsec.parser
- Libparser
  - Syntax
binsec.ppc64decoder
- Ppc64decoder
  - Ppc64ToDba
  - Ppc64_options
    
    Logger
binsec.smt
- Smt
  - Smt_external
    
    Solver
    
    Translate
  - Smt_internal
    
    Make
    
    F
    
    Ax
    
    Bl
    
    Bv
  - Smt_options
    
    Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    Debug_level
    
    KeepGoing
    
    Logger
    
    Loglevel
    
    Quiet
    
    SMTSolver
    
    SMT_dir
    
    SMT_log_directory
  - Smt_sig
    
    Solver
  - Smt_solver
  - Smt_symbolic
    
    State
binsec.smt.solver
- Libsolver
  - F
    
    Ax
    
    Bl
    
    Bv
  - S
    
    Ax
    
    Bl
    
    Bv
  - TERM
    
    Ax
    
    Bl
    
    Bv
binsec.sse
- Libsse
  - Cse
    
    Env
    
    Expr
    
    Layer
    
    Store
  - Dcode
    
    Make
    
    CALLBACK
    
    Fiber
    
    Path
    
    State
    
    Uid
    
    Value
    
    Stats
  - Eval
    
    Make
    
    Path
    
    State
    
    Uid
    
    Value
    
    Raw
    
    State
    
    Uid
    
    Value
  - Exec
    
    EXTENSION
    
    PLUGIN
    
    Run
    
    SF
    
    QS
    
    Preprocess
    
    Solver
    
    Uid
    
    Value
    
    W
  - Fiber
    
    S
  - Heuristic
    
    Bfs
    
    Dfs
    
    Nurs
  - Ir
    
    GRAPH
    
    E
    
    V
  - Opt
    
    Flags
  - Options
    
    AlternativeEngine
    
    Cse
    
    Engine
    
    JumpEnumDepth
    
    KillFlagsAtReturn
    
    LegacyEngine
    
    Logger
    
    MaxDepth
    
    MissingSymbol
    
    Monitor
    
    QMerge
    
    Randomize
    
    ScriptFiles
    
    Search_heuristics
    
    Seed
    
    Timeout
    
    TransientEnum
  - Path
    
    Make
    
    S
  - Probe
  - Screen
    
    Make
    
    E
    
    Q
    
    Preprocess
    
    Solver
  - Script
    
    Expr
    
    Instr
    
    Loc
    
    Output
    
    Symbol
  - Stats
    
    Exploration
    
    Query
    
    Preprocess
    
    Solver
  - Types
    
    A
    
    EXPLORATION_STATISTICS
    
    EXPLORATION_STATISTICS_FULL
    
    Output
    
    QUERY_STATISTICS
    
    Preprocess
    
    Solver
    
    RAW_STATE
    
    Uid
    
    Value
    
    STATE
    
    Uid
    
    Value
    
    STATE_FACTORY
    
    QS
    
    Preprocess
    
    Solver
    
    Uid
    
    Value
    
    UID
    
    VALUE
    
    WORKLIST
binsec.sse.checkct
- Checkct
  - Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
  - ChosenValues
  - Ct_state
  - Debug_level
  - Kind
  - LeakInfo
  - Logger
  - Loglevel
  - Make
    
    Options
    
    Path
    
    State
    
    Uid
    
    Value
    
    Stats
  - OPTIONS
  - Quiet
  - Relse
  - Report
  - StatsFile
  - Status
  - Taint
binsec.sse.formula
- Libformula
  - Sse_symbolic
    
    State
    
    QS
    
    Preprocess
    
    Solver
    
    S
    
    Uid
    
    Value
binsec.sse.shadow_stack
- Shadow_stack
  - Builder
    
    Any
    
    P
    
    Any_opt
    
    P
    
    Boolean
    
    P
    
    False
    
    P
    
    Float
    
    P
    
    Float_list
    
    P
    
    Float_option
    
    P
    
    Float_set
    
    P
    
    Integer
    
    P
    
    Integer_list
    
    P
    
    Integer_option
    
    P
    
    Integer_set
    
    P
    
    No
    
    P
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
  - Builtin
    
    P
    
    S
    
    Uid
    
    Value
  - Debug_level
  - Inline
    
    P
    
    S
    
    Uid
    
    Value
  - Logger
  - Loglevel
  - Mode
  - Quiet
binsec.sse.term
- Libterm
  - Ai
    
    CONTEXT
    
    Make
    
    C
    
    D
    
    S
  - Api_solver
    
    CONTEXT
    
    Context
    
    S
    
    Ax
    
    Bl
    
    Bv
    
    Make
    
    F
    
    Ax
    
    Bl
    
    Bv
    
    Open
  - Memory_manager
    
    CONTEXT
    
    Make
    
    C
    
    D
  - Senv
    
    State
    
    D
    
    QS
    
    Preprocess
    
    Solver
    
    Solver
    
    QS
    
    Preprocess
    
    Solver
    
    Uid
    
    Value
  - Sexpr
    
    Chunk
    
    Expr
    
    Memory
    
    Model
    
    Store
  - Smt2_solver
    
    Cross
    
    Printer
    
    Solver
  - Solver
    
    GET_MODEL
    
    GET_MODEL_WITH_STATS
    
    QS
    
    Preprocess
    
    Solver
    
    MultiChecks
    
    QS
    
    Preprocess
    
    Solver
    
    Session
    
    OPEN
    
    Once
    
    QS
    
    Preprocess
    
    Solver
    
    Session
    
    S
binsec.sse_register
- Sse

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module P : Program

Signature

exception AssertFailure of Dba.address

exception EndOfTrace of Env.t

val step : Env.t -> Dba.address -> Dba.Instr.t -> Env.t * Dba.address

val fetch : P.t -> Dba.address -> Dba.Instr.t