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

Authors

Maintainers

B

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

Sources

binsec-0.11.0.tbz

sha256=4cf70a0367fef6f33ee3165f05255914513ea0539b94ddfef0bd46fc9b42fa8a

sha512=cd67a5b7617f661a7786bef0c828ee55307cef5260dfecbb700a618be795d81b1ac49fc1a18c4904fd2eb8a182dc862b0159093028651e78e7dc743f5babf9e3

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