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

Authors

Maintainers

B

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

Sources

binsec-0.11.2.tbz

sha256=b758f3428b62a03103403196af99a5bb7df77a35afbcc5ce2d2b1fbe6d2ab36b

sha512=afa4fdf09ae0c2ab02530d674f9f2c1473d156e0438b4cb9c262ffea2d98c448251de55cd6fb176562edaae3897aeabe873ffa1ad47f861c75e1943792d90261

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