State (soteria-rust.Soteria_rust_lib.State.StateM.Make.State)

module Sptr : Sptr.S

type full_ptr := Sptr.t Rust_val.full_ptr

type rust_val := Sptr.t Rust_val.rust_val

include Soteria.Sym_states.Base.M(Rustsymex).S

type t

val show : t -> Ppx_deriving_runtime.string

module SM : 
  Soteria.Sym_states.State_monad.S
    with module Symex = Rustsymex
     and module Value = Rustsymex.Value
     and type st = t option

type syn

val pp_syn : 
  Ppx_deriving_runtime.Format.formatter ->
  syn ->
  Ppx_deriving_runtime.unit

val show_syn : syn -> Ppx_deriving_runtime.string

val to_syn : t -> syn list

val ins_outs : syn -> Rustsymex.Value.Expr.t list * Rustsymex.Value.Expr.t list

val produce : syn -> t option -> t option Rustsymex.Producer.t

val consume : syn -> t option -> (t option, syn list) Rustsymex.Consumer.t

type 'a ret := ('a, Error.with_trace, syn list) SM.Result.t

val pp : t Fmt.t

val pp_pretty : ignore_freed:bool -> t Fmt.t

Prettier but expensive printing.

val empty : t option

val load : ?ignore_borrow:bool -> full_ptr -> Charon.Types.ty -> rust_val ret

val tb_load : full_ptr -> Charon.Types.ty -> unit ret

val load_discriminant : 
  full_ptr ->
  Charon.Types.ty ->
  Charon.Types.variant_id ret

val store : full_ptr -> Charon.Types.ty -> rust_val -> unit ret

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 ->
  full_ptr ret

val alloc_ty : 
  ?kind:Common.Alloc_kind.t ->
  ?span:Charon.Meta.span_data ->
  Charon.Types.ty ->
  full_ptr ret

val alloc_tys : 
  ?kind:Common.Alloc_kind.t ->
  ?span:Charon.Meta.span_data ->
  Charon.Types.ty list ->
  full_ptr list ret

val free : full_ptr -> unit ret

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)
    ret

val fake_read : full_ptr -> Charon.Types.ty -> unit ret

val check_non_dangling : full_ptr -> Charon.Types.ty -> unit ret

val check_ptr_align : full_ptr -> Charon.Types.ty -> unit ret

val copy_nonoverlapping : 
  src:full_ptr ->
  dst:full_ptr ->
  size:Soteria_rust_lib.Typed.T.sint Typed.t ->
  unit ret

val uninit : full_ptr -> Charon.Types.ty -> unit ret

val zeros : full_ptr -> Soteria_rust_lib.Typed.T.sint Typed.t -> unit ret

val with_decay_map : 'a Sptr.DecayMapMonad.t -> 'a SM.t

val store_str_global : string -> full_ptr -> unit ret

val store_global : Charon.Types.global_decl_id -> full_ptr -> unit ret

val load_str_global : string -> full_ptr option ret

val load_global : Charon.Types.global_decl_id -> full_ptr option ret

val borrow : ?protect:bool -> full_ptr -> Charon.Types.ty -> full_ptr ret

val unprotect : full_ptr -> Charon.Types.ty -> unit ret

val with_exposed : [< Soteria_rust_lib.Typed.T.sint ] Typed.t -> full_ptr ret

val leak_check : unit -> unit ret

val add_error : Error.with_trace -> unit ret

val pop_error : unit -> 'a ret

val declare_fn : Common.Fun_kind.t -> full_ptr ret

val lookup_fn : full_ptr -> Common.Fun_kind.t ret

val lookup_const_generic : 
  Charon.Types.const_generic_var_id ->
  Charon.Types.ty ->
  rust_val ret

val register_thread_exit : (unit -> unit ret) -> unit ret

val run_thread_exits : unit -> unit ret