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 (20)

Authors

Maintainers

B

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

Sources

binsec-0.11.1.tbz

sha256=bb48234a4b60a872015a88282df4873f01dcc984753d49ad2583d49c1ae7d705

sha512=e8aa47a736b83bfd47d5b5e96d0988859b4873ad4a112fee7cd21d02bc72ecec61b7de610a959e38d2f2f5eef8082a2c100c201e5eae5ae3a880c747dce6ae63

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).