package binsec

You can search for identifiers within the package.

in-package search v0.2.0

package binsec

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
  - Bbsse_backward
    
    Backward
    
    Env
    
    Eval
    
    G
    
    Directives
    
    Enumeration
    
    Path
    
    PredicatSet
    
    Stats
    
    R
  - Bbsse_bb_paths
    
    Path_generator
  - Bbsse_lexer
  - Bbsse_options
    
    Address_counter
    
    FindJumps
    
    GenGroundTruth
    
    IgnoreAddr
    
    Logger
    
    MaxCondition
    
    MaxConditionCycle
    
    MaxDepth
    
    OPFile
    
    ProcessAllJumps
    
    Visit_address_counter
  - Bbsse_parser
  - Bbsse_smt
    
    Query_stats
    
    Solver
    
    Translate
  - Bbsse_types
    
    Bfs_global
    
    Directives
    
    Enumeration
    
    Path
    
    C
    
    E
    
    Fixpoint
    
    X
    
    V
    
    Dfs_global
    
    Directives
    
    Enumeration
    
    Path
    
    Extra
    
    GLOBAL_ENV
    
    Directives
    
    Enumeration
    
    Path
    
    Nurs_global
    
    Directives
    
    Enumeration
    
    Path
    
    Path_state
  - Binpatcher
    
    PatchMap
    
    WritableLoader
  - Binpatcher_options
    
    Logger
    
    PatchFile
    
    PatchOutFile
  - Binstream
  - Bitset
  - Bitvector
    
    Collection
    
    Hamt
    
    Htbl
    
    Map
    
    Set
    
    Common
  - Bw_main
  - Bw_options
    
    K
    
    Logger
    
    Opaque_addresses
    
    Opaque_predicates
    
    Opaque_sections
  - Cfg
    
    Make
    
    A
    
    E
    
    Fixpoint
    
    X
    
    V
    
    S
    
    E
    
    Fixpoint
    
    X
    
    V
  - Cfgraph
    
    Dot
    
    G
    
    E
    
    V
  - 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
    
    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
    
    Printing
  - Formula_decoder
    
    Instr_to_Formula
    
    Binary
    
    Boolean
    
    State
  - 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
  - Fstack
    
    Make
    
    X
    
    Typed
  - Generic_decoder
    
    Decode_Expr
    
    I
    
    Binary
    
    Boolean
    
    M
    
    Decode_Instr
    
    S
    
    Binary
    
    Boolean
    
    State
  - Generic_decoder_sig
    
    Expr_Input
    
    Binary
    
    Boolean
    
    M
    
    Instr_Input
    
    Binary
    
    Boolean
    
    State
    
    Monad
    
    Monadic_Arity
    
    M
    
    State_Monad
    
    State
  - Ghidra_cfg
    
    E
    
    V
  - 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
  - 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
  - Lexer_infos
  - List_utils
  - Loader
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
  - Loader_buf
    
    Bufferable
    
    Make
    
    B
    
    Peek
    
    Read
    
    Peek
    
    Read
    
    S
    
    Peek
    
    Read
    
    W
    
    Peek
    
    Read
    
    Write
    
    Wake
    
    Peek
    
    Read
    
    W
    
    Write
    
    Writable
    
    Write
  - Loader_dump
    
    Address
    
    Peek
    
    Read
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Section
    
    Symbol
  - Loader_elf
    
    Address
    
    Peek
    
    Read
    
    E_class
    
    E_ident
    
    Ehdr
    
    ET
    
    Img
    
    Offset
    
    Peek
    
    Read
    
    Phdr
    
    Section
    
    Shdr
    
    SHF
    
    SHN
    
    SHT
    
    Sym
    
    STB
    
    STT
    
    Symbol
  - Loader_pe
    
    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
  - Opaque
    
    Check
    
    Opacity_status
  - Parse_helpers
    
    Declarations
    
    Initialization
    
    Message
    
    Value
    
    Mk
    
    Permissions
    
    Predicates
  - Parse_utils
  - Parsepin
  - Parser
  - Parser_ghidra
  - Parser_infos
  - Predba
  - Prettytbl
    
    Column
  - Print_utils
  - Prover
    
    Command
  - Riscv_arch
    
    Mode
    
    S
    
    V128
    
    V32
    
    V64
  - Riscv_options
    
    Logger
    
    Odump_file
  - Riscv_to_dba
  - Runtime
    
    Sites
  - Senv
    
    Query_stats
  - 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
  - Sse
  - Sse_graph
    
    G
    
    E
    
    Fixpoint
    
    X
    
    V
  - Sse_lexer
  - Sse_options
    
    AddressTraceFile
    
    Address_counter
    
    AvoidAddresses
    
    Comment
    
    Directives
    
    Dot_filename_out
    
    GoalAddresses
    
    JumpEnumDepth
    
    KeepGoing
    
    LoadROSections
    
    LoadSections
    
    Logger
    
    MaxDepth
    
    MemoryFile
    
    Randomize
    
    SMT_dir
    
    SMT_log_directory
    
    ScriptFiles
    
    Search_heuristics
    
    Seed
    
    Solver_call_frequency
    
    Timeout
    
    Visit_address_counter
  - Sse_pack
  - Sse_parser
    
    Make
    
    E
  - Sse_prune
    
    Distance
  - Sse_smt
    
    Translate
  - Sse_symbolic
    
    State
  - Sse_tokens
  - Sse_types
    
    Bfs
    
    C
    
    E
    
    Fixpoint
    
    X
    
    V
    
    Dfs
    
    Nurs
    
    Path_state
    
    Pragma
    
    Script
    
    WORKLIST
  - Sse_utils
  - String_utils
  - Subprocess
  - Transfer_functions
    
    Arity
    
    Binary_Backward
    
    Arity
    
    Binary_Forward
    
    Arity
    
    Boolean_Backward
    
    Arity
    
    Boolean_Forward
    
    Arity
  - Utils
  - Virtual_address
    
    Hamt
    
    Htbl
    
    Map
    
    Set
  - Worklist
    
    CMake
    
    X
    
    Make
    
    X
    
    S
  - X86Instruction
  - X86Types
  - X86Util
  - X86_options
    
    HandleSegments
    
    Logger
    
    ProtectedMode
  - X86decoder
  - X86pp
  - X86toDba
  - Xtrasec
    
    Make
    
    Param
    
    Binary
    
    Boolean
    
    State
  - Xtrasec_options
    
    Concretize_mem
    
    Concretize_regs
    
    Logger
    
    Output_smt
    
    Trace_file

Legend:
Library
Module
Module type
Parameter
Class
Class type

Translation functions from BINSEC inner representation to SMT-LIB terms

val bl_term : Formula.bl_term -> Smtlib.term

val bv_term : Formula.bv_term -> Smtlib.term

val ax_term : Formula.ax_term -> Smtlib.term

val term : Formula.term -> Smtlib.term

val entry : Formula.entry -> Smtlib.command

val formula : Formula.formula -> Smtlib.script