package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

dune-project

Dependency

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

Authors

Maintainers

B

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

Sources

binsec-0.11.3.tbz

sha256=93f6fe439d486b166062ef6dd92c4ce3aa0947b5e18b1c3aa7de2fc3003aa6d9

sha512=98feb2b0a3f0a33fe912e9885311dd1c051768c707437f8ef038a8489fec019960142b588c6973eb8f726a14d9b2a1b4c765d915539911cb9f6ed6da9f1e51f2

doc/binsec.symbolic/Binsec_symbolic/Evaluator/Make/argument-2-State/index.html

Parameter `Make.State`

type t

A mapping for variables (Binsec_kernel.Dba.Var.t -> value) and memory accesses (value -> value).

val lookup : Binsec_kernel.Dba.Var.t -> t -> Value.t

lookup var s returns the value assigned to var in s.

raises Undefined
if var is not in s.

val read : 
  addr:Value.t ->
  int ->
  Binsec_kernel.Machine.endianness ->
  t ->
  Value.t * t

read ~addr len d s returns len bytes of the value stored at address addr in the main memory array @, together with the updated state s. The byte order is determined by the endianness d.

raises Undeclared
None if there is no main memory in s (see S.declare).

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

select m ~addr len d s returns len bytes of the value stored at address addr in the memory array m, together with the updated state s. The byte order is determined by the endianness d.

raises Undeclared
Some m if m is not in s (see S.declare).