Module Soteria_rust_lib.Store

module Map : sig ... end
type 'a binding_kind =
  1. | Stackptr of 'a Rust_val.full_ptr
  2. | Value of 'a Rust_val.t
  3. | Uninit
  4. | Dead

We have four kinds of bindings:

  • Stackptr: the symbol is bound to a stack pointer, that lives in the heap.
  • Value: the symbol is bound to an immediate value; it does not have an address.
  • Uninit: the symbol is bound to an immediate, uninitialized value.
  • Dead: the symbol is dead; it doesn't exist (e.g. after a StorageDead).
val pp_binding_kind : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'a binding_kind -> Ppx_deriving_runtime.unit
val show_binding_kind : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> 'a binding_kind -> Ppx_deriving_runtime.string
type 'a binding = {
  1. kind : 'a binding_kind;
  2. ty : Charon.Types.ty;
}
val pp_binding : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'a binding -> Ppx_deriving_runtime.unit
val show_binding : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> 'a binding -> Ppx_deriving_runtime.string
type 'a t = 'a binding Map.t
val reserve : Map.key -> Charon.Types.ty -> 'a binding Map.t -> 'a binding Map.t
val declare : Map.key -> 'a binding_kind -> 'a binding Map.t -> 'a binding Map.t
val declare_value : Map.key -> 'a Rust_val.t -> 'a binding Map.t -> 'a binding Map.t
val declare_ptr : Map.key -> 'a Rust_val.full_ptr -> 'a binding Map.t -> 'a binding Map.t
val declare_uninit : Map.key -> 'a binding Map.t -> 'a binding Map.t
val dealloc : Map.key -> 'a binding Map.t -> 'a binding Map.t
val get_ty : Map.key -> 'a binding Map.t -> Charon.Types.ty
val find : Map.key -> 'a t -> 'a binding
val empty : 'a Map.t
val bindings : 'a t -> (Map.key * 'a binding) list