package owi

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

include module type of struct include Symbolic_memory end

type t = Symbolic_memory.t

type collection = Symbolic_memory.collection

val init : unit -> collection

val clone : collection -> collection

val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t

val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit

val free : t -> Int32.t -> unit

val grow : t -> Smtml.Expr.t -> unit

val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t

val blit : 
  t ->
  src:Smtml.Expr.t ->
  dst:Smtml.Expr.t ->
  len:Smtml.Expr.t ->
  Smtml.Expr.t

val blit_string : 
  t ->
  string ->
  src:Smtml.Expr.t ->
  dst:Smtml.Expr.t ->
  len:Smtml.Expr.t ->
  Smtml.Expr.t

val size : t -> Smtml.Expr.t

val size_in_pages : t -> Smtml.Expr.t

val get_limit_max : t -> Smtml.Expr.t option

module ITbl = Symbolic_memory.ITbl

val iter : (t ITbl.t -> unit) -> collection -> unit

val concretise : Smtml.Expr.t -> Smtml.Expr.t Choice.t

val check_within_bounds : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val with_concrete : 
  t ->
  Smtml.Expr.t ->
  (t -> Symbolic_value.int32 -> 'a) ->
  'a0 Choice.t

val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t

val store_8 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit Choice.t

val store_16 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit Choice.t

val store_32 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit Choice.t

val store_64 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit Choice.t