owi 0.2 (latest) · OCaml Package

type t

type 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 : sig ... end

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

val concretise : Smtml.Expr.t -> Smtml.Expr.t Symbolic_choice.Minimalist.t

val check_within_bounds : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

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

val load_8_s : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

val load_8_u : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

val load_16_s : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

val load_16_u : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

val load_32 : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

val load_64 : 
  t ->
  Smtml.Expr.t ->
  Symbolic_value.int32 Symbolic_choice.Minimalist.t

val store_8 : 
  t ->
  addr:Smtml.Expr.t ->
  Smtml.Expr.t ->
  unit Symbolic_choice.Minimalist.t

val store_16 : 
  t ->
  addr:Smtml.Expr.t ->
  Smtml.Expr.t ->
  unit Symbolic_choice.Minimalist.t

val store_32 : 
  t ->
  addr:Smtml.Expr.t ->
  Smtml.Expr.t ->
  unit Symbolic_choice.Minimalist.t

val store_64 : 
  t ->
  addr:Smtml.Expr.t ->
  Smtml.Expr.t ->
  unit Symbolic_choice.Minimalist.t

package owi