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 getter : 'a Libsse.Types.feature -> (t -> 'a) option

getter feature returns a getter function from a state to an extended feature. It returns None if the current implementation does not support the queried feature.

Sourceval setter : 'a Libsse.Types.feature -> ('a -> t -> t) option

setter feature returns a setter function to update an extended feature. It returns None if the current implementation does not support the queried feature.

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Senv.State`Source

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