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

sha256=a6ccc9c0a756f6056a5bf6a2f602d59690944f4164cc180d0082c36f081e7e94

sha512=cd85654f94da9ce8fedab746c557c326821cc7932005337303607e0c52d7caf403655fc1000b34d32f1f2606ab1b3d079b9057346ef0a2f88057e0dd7b412cce

doc/libterm/Libterm/Senv/State/index.html

Module `Senv.State`Source

Parameters

module D : Domains.S

module Solver : Solver.GET_MODEL_WITH_STATS

module QS : Libsse.Types.QUERY_STATISTICS

Signature

Sourcetype t

Symbolic state

Sourcemodule Uid : Libsse.Types.UID

Source

module Value : 
  Libsse.Types.VALUE
    with type id := Uid.t
     and type state := t
    with type t = Sexpr.Expr.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/libterm/Libterm/Senv/State/index.html

Module Senv.StateSource

Parameters

Signature

Module `Senv.State`Source