M (soteria-rust.Soteria_rust_lib.Builtins.Miri.M)

Parameters

module StateM : State.StateM.S

Signature

module Alloc : sig ... end

val alloc_id : 
  ('a, 'b, StateM.Sptr.t) Rust_val.raw list ->
  (([> Soteria_rust_lib.Typed.T.sint ] Typed.t, 'c, 'd) Rust_val.raw, 'e)
    StateM.t

val promise_alignement : 
  ([< Soteria_rust_lib.Typed.T.any ] Typed.t, 'a, StateM.Sptr.t) Rust_val.raw
    list ->
  (('b, 'c, 'd) Rust_val.raw, 'e) StateM.t

val alloc : 
  ([< Soteria_rust_lib.Typed.T.any ] Typed.t, 'a, 'b) Rust_val.raw list ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t, 'c, StateM.Sptr.t) Rust_val.raw, 'd)
    StateM.t

val dealloc : 
  (Soteria_rust_lib.Typed.T.sint Typed.t, 'a, StateM.Sptr.t) Rust_val.raw list ->
  (('b, 'c, 'd) Rust_val.raw, 'e) StateM.t