package binsec

You can search for identifiers within the package.

in-package search v0.2.0

binsec
- Binsec
  - Array_utils
  - Astbuilder
    
    Env
  - Base_logger
  - Basic_types
    
    BigInt
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Collection_make
    
    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
    
    I
    
    S
    
    V
    
    S
    
    E
    
    Fixpoint
    
    X
    
    V
  - Cfgraph
    
    Dot
    
    Edge
    
    G
    
    E
    
    V
    
    Node
  - Cli
    
    BOOLEAN
    
    Boot
    
    CHECKABLE
    
    CLI_DECL
    
    Cli_sig
    
    Builder
    
    Any
    
    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
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    True
    
    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
    
    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
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    True
    
    P
    
    Variant_choice
    
    P
    
    Variant_choice_assoc
    
    P
    
    Variant_list
    
    P
    
    Zero
    
    P
    
    D
    
    Debug_level
    
    Logger
    
    Loglevel
    
    Quiet
    
    Options
    
    Builder
    
    Any
    
    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
    
    String
    
    P
    
    String_choice
    
    P
    
    String_list
    
    P
    
    String_option
    
    P
    
    String_set
    
    P
    
    True
    
    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
    
    VarTag
  - 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
    
    Map
    
    Logger
    
    Region
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Rights
    
    Statement
  - Dba_utils
    
    Expr
  - Dba_visitor
    
    dba_inplace_visitor
    
    inplace_visitor_t
  - Dbacsl_parser
  - Dbacsl_token
  - Decode_utils
  - Dhunk
    
    Check
    
    Node
    
    Simplify
  - 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
    
    IgnoreUnhandledInstructions
    
    Logger
    
    NoLoaderMode
    
    OpcodeOutputFile
    
    Sections
    
    ShowInstructionCount
    
    SimplifiedDisassembly
  - Dwarf
  - Dwarf_cunit
    
    Func
    
    Global
    
    Type
    
    Var
  - Dwarf_expr
  - Dwarf_frame
  - Dwarf_lines
  - Dwarf_options
    
    Logger
  - Elf_options
    
    Alloc
    
    Logger
    
    Reloc
  - Errors
  - File_utils
  - Formula
    
    AxTermHashtbl
    
    AxVarHashtbl
    
    AxVarSet
    
    BlTermHashtbl
    
    BlVarHashtbl
    
    BlVarSet
    
    BvTermHashtbl
    
    BvVarHashtbl
    
    BvVarSet
    
    Printing
    
    VarSet
  - Formula_main
  - Formula_options
    
    Flatten_memory
    
    Logger
    
    No_stitching
    
    OptimAll
    
    OptimCst
    
    OptimItv
    
    OptimLst
    
    OptimPrn
    
    OptimRbs
    
    OptimRow
    
    OptimSsa
    
    Solver
    
    Options
    
    Timeout
  - Formula_pp
  - Formula_to_smtlib
  - Formula_transformation
  - Formula_utils
    
    BindEnv
  - Ghidra_cfg
    
    E
    
    V
  - Ghidra_options
    
    Cache
    
    Logger
    
    Runner
  - Hash
  - Hashamt
    
    Make
    
    H
    
    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
    
    H
    
    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
  - Lexer_infos
  - List_utils
  - 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
  - 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_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
    
    Permissions
    
    Predicates
  - Parse_utils
  - Parser
  - Parser_ghidra
  - Parser_infos
  - Predba
  - Prettytbl
    
    Column
  - Print_utils
  - Prover
    
    Command
  - Riscv_arch
    
    Mode
    
    Register
    
    M
    
    RegisterSize
    
    S
  - Riscv_options
    
    Logger
    
    Odump_file
  - Riscv_to_dba
  - Runtime
    
    Sites
  - Sequence
  - Sigs
    
    ANY
    
    Arithmetic
    
    Bitwise
    
    COMPARABLE
    
    Collection
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Comparisons
    
    EXTENDED_LOGICAL
    
    Eq
    
    HASHABLE
    
    HASHABLE_AUTO
    
    ITERABLE
    
    Logical
    
    PRINTABLE
    
    SHIFT_ROT
    
    STRINGIFIABLE
    
    STR_INJECTIBLE
  - Simplification_dba
  - Simplification_dba_block
    
    Constant_propagation
    
    DC_elimination
  - Simplification_dba_prog
  - Simplification_dba_utils
  - Simplification_options
    
    Display_statistics
    
    Logger
    
    Simplification
  - 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
  - Solver
    
    Command
    
    Session
  - String_utils
  - Subprocess
  - Term
    
    Bv
    
    Collection
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Common
    
    Make
    
    A
    
    B
    
    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
binsec.amd64decoder
- Amd64decoder
  - Amd64ToDba
  - Amd64_options
    
    Logger
binsec.armv7decoder
- Armv7decoder
  - ArmToDba
  - Arm_options
    
    Logger
    
    SupportedModes
binsec.armv8decoder
- Armv8decoder
  - Aarch64ToDba
  - Aarch64_options
    
    Logger
binsec.smt
- Smt
  - Smt_bitwuzla
  - Smt_bitwuzla_utils
  - Smt_external
    
    Solver
    
    Translate
  - Smt_options
    
    KeepGoing
    
    Logger
    
    SMTSolver
    
    SMT_dir
    
    SMT_log_directory
  - Smt_sig
    
    Solver
  - Smt_solver
  - Smt_symbolic
    
    State
  - Suid
binsec.sse
- Se
  - Native_solver
    
    Solver
  - Senv
    
    State
    
    F
    
    QS
    
    Preprocess
    
    Solver
  - Sexpr
    
    AxTbl
    
    BvTbl
    
    Expr
    
    Memory
  - Smt2_solver
    
    Cross
    
    Printer
    
    Solver
  - Solver_sig
    
    FACTORY
    
    S
  - Sse
  - Sse_lexer
  - Sse_options
    
    Address_counter
    
    AlternativeEngine
    
    AvoidAddresses
    
    Comment
    
    Directives
    
    Dot_filename_out
    
    GoalAddresses
    
    JumpEnumDepth
    
    LoadROSections
    
    LoadSections
    
    Logger
    
    MaxDepth
    
    MemoryFile
    
    Randomize
    
    ScriptFiles
    
    Search_heuristics
    
    Seed
    
    Solver_call_frequency
    
    Timeout
    
    TransientEnum
    
    Visit_address_counter
  - Sse_parser
    
    Make
    
    E
  - Sse_screen
    
    Make
    
    E
    
    Q
    
    Preprocess
    
    Solver
  - Sse_symbolic
    
    State
    
    QS
    
    Preprocess
    
    Solver
    
    S
  - Sse_tokens
  - Sse_types
    
    Bfs
    
    E
    
    C
    
    E
    
    Fixpoint
    
    X
    
    V
    
    Dfs
    
    E
    
    EXPLORATION_STATISTICS
    
    Nurs
    
    E
    
    Path_state
    
    S
    
    Pragma
    
    QUERY_STATISTICS
    
    Preprocess
    
    Solver
    
    STATE
    
    STATE_FACTORY
    
    QS
    
    Preprocess
    
    Solver
    
    Script
    
    WORKLIST
    
    WORKLIST_FACTORY
    
    E
  - Sse_utils

Legend:
Library
Module
Module type
Parameter
Class
Class type

val expr : 
  Smt_symbolic.State.t ->
  Binsec.Dba.Expr.t ->
  Binsec.Formula.bv_term * Smt_symbolic.State.t

missing bitvectors are implicitely declared so this returns a new symbolic state

val assign : 
  ?wild:bool ->
  Binsec.Dba.LValue.t ->
  Binsec.Dba.Expr.t ->
  Smt_symbolic.State.t ->
  Smt_symbolic.State.t

val havoc : 
  ?naming_hint:string ->
  ?wild:bool ->
  Binsec.Dba.LValue.t ->
  Smt_symbolic.State.t ->
  Smt_symbolic.State.t

val assume : Binsec.Dba.Expr.t -> Smt_symbolic.State.t -> Smt_symbolic.State.t