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

sha256=d959c2351b6cac10ffbdaf112769a676c9ad84bf6bc7fefa5cb1daa8d086cc97

sha512=1a3951896f05fb3a4cb05e81830373c75409a69c49323dc82e97c94889927b5f9561e704565a22c2a608842f67063d6c89a330477165b197a40d6ac231c09a7e

doc/libformula/Libformula/Sse_symbolic/State/index.html

Module `Sse_symbolic.State`Source

Parameters

module S : Smt.Smt_sig.Solver

module QS : Libsse.Types.QUERY_STATISTICS

Signature

Sourcetype t

Symbolic state

Sourcemodule Uid : Libsse.Types.UID

Sourcemodule Value : Libsse.Types.VALUE with type id := Uid.t and type state := 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/libformula/Libformula/Sse_symbolic/State/index.html

Module Sse_symbolic.StateSource

Parameters

Signature

Module `Sse_symbolic.State`Source