package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

Dune Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (18)

Authors

Maintainers

B

BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.8.1.tbz

sha256=94090e05906c7a0559f60d2c65dbe167eb5953a2338b958b71911c1c81dd9ffd

sha512=6f52f8918c3c242f1346ebdc244f80744966112b935e00519e5d4d5acc040f8e2d2c54ff6b172cf5eb34b9bf7366de085605de88fcc15c43f34abce39ed34220

doc/libterm/Libterm/Senv/State/index.html

Module `Senv.State`Source

Parameters

module D : Domains.S

module F : Solver_sig.FACTORY

module QS : Libsse.Types.QUERY_STATISTICS

Signature

Sourcetype t

Symbolic state

Sourcemodule Uid : Libsse.Types.UID

Source

module Value : 
  Libsse.Types.VALUE
    with type id := Uid.t
     and type state := t
    with type t = Sexpr.Expr.t

Sourceval lookup : Libsse.Types.Var.t -> t -> Value.t

Sourceval read : addr:Value.t -> int -> Binsec.Machine.endianness -> t -> Value.t * t

Source

val select : 
  string ->
  addr:Value.t ->
  int ->
  Binsec.Machine.endianness ->
  t ->
  Value.t * t

Sourceval empty : unit -> t

Sourceval assume : Value.t -> t -> t option

Sourceval test : Value.t -> t -> t Libsse.Types.test

Sourceval get_value : Value.t -> t -> Binsec.Bitvector.t

Sourceval get_a_value : Value.t -> t -> Binsec.Bitvector.t

Source

val enumerate : 
  Value.t ->
  ?n:int ->
  ?except:Binsec.Bitvector.t list ->
  t ->
  (Binsec.Bitvector.t * t) list

Sourceval alloc : array:string -> t -> t

Sourceval assign : Libsse.Types.Var.t -> Value.t -> t -> t

Sourceval write : addr:Value.t -> Value.t -> Binsec.Machine.endianness -> t -> t

Source

val store : 
  string ->
  addr:Value.t ->
  Value.t ->
  Binsec.Machine.endianness ->
  t ->
  t

Sourceval memcpy : addr:Binsec.Bitvector.t -> int -> Binsec.Loader_buf.t -> t -> t

Sourceval merge : parent:t -> t -> t -> t

Sourceval assertions : t -> Value.t list

Sourceval pp : Format.formatter -> t -> unit

Sourceval pp_smt : Value.t Libsse.Types.target -> Format.formatter -> t -> unit

Sourceval to_formula : t -> Binsec.Formula.formula

Sourceval downcast : 'a Libsse.Types.feature -> (t -> 'a) option

downcast feature returns a cast function from a state to an extended state. It returns None if the current implementation does not support the queried feature.

On This Page

Parameters
Signature

package binsec

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libterm/Libterm/Senv/State/index.html

Module Senv.StateSource

Parameters

Signature

Module `Senv.State`Source