package binsec

You can search for identifiers within the package.

in-package search v0.2.0

Semantic analysis of binary executables

Install

sha256=81859d54721969893aabcb5b16ff41d0698f8c24799d8357ec7b1c10cd5ebf94

sha512=580561e70189b3c77bf09364ad393750263b5cfb36dce01aa7cd34ea4d4ebcc9085a52f18b7514e4046d51b488f2dfc5271aea8259c7cbce1534b880cf76bb6e

include RAW_STATE

type t

Symbolic state

module Uid : UID

module Value : VALUE with type id := Uid.t and type state := t

val lookup : Var.t -> t -> Value.t

val read : addr:Value.t -> int -> Binsec.Machine.endianness -> t -> Value.t * t

val select : 
  string ->
  addr:Value.t ->
  int ->
  Binsec.Machine.endianness ->
  t ->
  Value.t * t

val empty : unit -> t

val assume : Value.t -> t -> t option

val test : Value.t -> t -> t test

val get_value : Value.t -> t -> Binsec.Bitvector.t

val get_a_value : Value.t -> t -> Binsec.Bitvector.t

val enumerate : 
  Value.t ->
  ?n:int ->
  ?except:Binsec.Bitvector.t list ->
  t ->
  (Binsec.Bitvector.t * t) list

val alloc : array:string -> t -> t

val assign : Var.t -> Value.t -> t -> t

val write : addr:Value.t -> Value.t -> Binsec.Machine.endianness -> t -> t

val store : 
  string ->
  addr:Value.t ->
  Value.t ->
  Binsec.Machine.endianness ->
  t ->
  t

val memcpy : addr:Binsec.Bitvector.t -> int -> Binsec.Loader_buf.t -> t -> t

val merge : parent:t -> t -> t -> t

val assertions : t -> Value.t list

val pp : Format.formatter -> t -> unit

val pp_smt : Value.t target -> Format.formatter -> t -> unit

val to_formula : t -> Binsec.Formula.formula

val id : Uid.t key

val symbols : Value.t list S.Map.t key