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.2.tbz

sha256=b8e7b9c756245656c481e992549fb7b1864ee6eeb492e16488e7a9d962d39cdb

sha512=07a5e4105e5275751fcc6832743f5f9eedc72bd061273ec54c4466135032852120df3784ba571656c788e5f3cd971aad8a53f030336a364e77e940e26dff38d7

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