Module StateM.State

val empty : st
val load : ?ignore_borrow:bool -> full_ptr -> Charon.Types.ty -> (rust_val, 'env) t
val load_discriminant : full_ptr -> Charon.Types.ty -> (Charon.Types.variant_id, 'env) t
val store : full_ptr -> Charon.Types.ty -> rust_val -> (unit, 'env) t
val zeros : full_ptr -> Soteria_rust_lib.Typed.T.sint Typed.t -> (unit, 'env) t
val alloc_ty : ?kind:Common.Alloc_kind.t -> ?span:Charon.Meta.span_data -> Charon.Types.ty -> (full_ptr, 'env) t
val alloc_tys : ?kind:Common.Alloc_kind.t -> ?span:Charon.Meta.span_data -> Charon.Types.ty list -> (full_ptr list, 'env) t
val alloc_untyped : ?kind:Common.Alloc_kind.t -> ?span:Charon.Meta.span_data -> zeroed:bool -> size:Soteria_rust_lib.Typed.T.sint Typed.t -> align:Soteria_rust_lib.Typed.T.nonzero Typed.t -> unit -> (full_ptr, 'env) t
val copy_nonoverlapping : src:full_ptr -> dst:full_ptr -> size:Soteria_rust_lib.Typed.T.sint Typed.t -> (unit, 'env) t
val uninit : full_ptr -> Charon.Types.ty -> (unit, 'env) t
val free : full_ptr -> (unit, 'env) t
val check_ptr_align : full_ptr -> Charon.Types.ty -> (unit, 'env) t
val borrow : ?protect:bool -> full_ptr -> Charon.Types.ty -> (full_ptr, 'env) t
val unprotect : full_ptr -> Charon.Types.ty -> (unit, 'env) t
val with_exposed : [< Soteria_rust_lib.Typed.T.sint ] Typed.t -> (full_ptr, 'env) t
val tb_load : full_ptr -> Charon.Types.ty -> (unit, 'env) t
val load_global : Charon.Types.global_decl_id -> (full_ptr option, 'env) t
val store_global : Charon.Types.global_decl_id -> full_ptr -> (unit, 'env) t
val load_str_global : string -> (full_ptr option, 'env) t
val store_str_global : string -> full_ptr -> (unit, 'env) t
val declare_fn : Common.Fun_kind.t -> (full_ptr, 'env) t
val lookup_fn : full_ptr -> (Common.Fun_kind.t, 'env) t
val lookup_const_generic : Charon.Types.const_generic_var_id -> Charon.Types.ty -> (rust_val, 'env) t
val register_thread_exit : (unit -> (unit, unit) t) -> (unit, 'env) t
val run_thread_exits : unit -> (unit, 'env) t
val add_error : Error.with_trace -> (unit, 'env) t
val pop_error : unit -> ('a, 'env) t
val leak_check : unit -> (unit, 'env) t
val fake_read : full_ptr -> Charon.Types.ty -> (unit, 'env) t
val check_non_dangling : full_ptr -> Charon.Types.ty -> (unit, 'env) t
val size_and_align_of_val : Charon.Types.ty -> Sptr.t Rust_val.meta -> (Soteria_rust_lib.Typed.T.sint Typed.t * Soteria_rust_lib.Typed.T.nonzero Typed.t, 'env) t