Sptr (soteria-rust.Soteria_rust_lib.Analyses.Wpst.Interp.StateM.Sptr)

type t = State.Sptr.t

val pp : 
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

val fresh : 
  unit ->
  Soteria_rust_lib__Sptr.DecayMap.t ->
  (t * Soteria_rust_lib__Sptr.DecayMap.t) Rustsymex.t

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

val subst : (Rustsymex.Value.Expr.t -> 'a Rustsymex.Value.t) -> syn -> t

val learn_eq : 
  syn ->
  t ->
  (unit, 'a) Soteria_rust_lib__Sptr.DecayMapMonad.Consumer.t

val exprs_syn : syn -> Rustsymex.Value.Expr.t list

val null_ptr : unit -> t

val null_ptr_of : [< Soteria_rust_lib.Typed.T.sint ] Typed.t -> t

val sem_eq : t -> t -> Soteria_rust_lib.Typed.T.sbool Typed.t

val is_at_null_loc : t -> Soteria_rust_lib.Typed.T.sbool Typed.t

val is_same_loc : t -> t -> Soteria_rust_lib.Typed.T.sbool Typed.t

val constraints : t -> Soteria_rust_lib.Typed.T.sbool Typed.t

val nondet : Charon.Types.ty -> (t, [> Error.t ], 'a) Rustsymex.Result.t

val as_id : t -> [> Soteria_rust_lib.Typed.T.sint ] Typed.t

val is_aligned : 
  Soteria_rust_lib.Typed.T.nonzero Typed.t ->
  t ->
  [> Soteria_rust_lib.Typed.T.sbool ] Typed.t * Error.t

val allocation_info : 
  t ->
  [> Soteria_rust_lib.Typed.T.sint ] Typed.t
  * [> Soteria_rust_lib.Typed.T.nonzero ] Typed.t

val offset : 
  ?check:bool ->
  ?ty:Charon.Types.ty ->
  signed:bool ->
  t ->
  [< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (t, 'env) t

val project : 
  Charon.Types.ty ->
  Charon.Expressions.field_proj_kind ->
  Charon.Types.field_id ->
  t ->
  (t, 'env) t

val distance : t -> t -> (Soteria_rust_lib.Typed.T.sint Typed.t, 'env) t

val decay : t -> (Soteria_rust_lib.Typed.T.sint Typed.t, 'env) t

val expose : t -> (Soteria_rust_lib.Typed.T.sint Typed.t, 'env) t