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

include Sptr.S

pointer type

include Sptr.D_abstr.S_with_syn

type t

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

val show : t -> Ppx_deriving_runtime.string

val fresh : unit -> t Sptr.DecayMapMonad.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 : 
  (Sptr.DecayMapMonad.Value.Expr.t -> 'a Sptr.DecayMapMonad.Value.t) ->
  syn ->
  t

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

val exprs_syn : syn -> Sptr.DecayMapMonad.Value.Expr.t list

include Sptr.D_abstr.Sem_eq with type t := t

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

Pointer equality. This comparison is structural, i.e. it is aware of provenance.

In other words, given addr = decay ptr and ptr' = of_exposed addr, sem_eq ptr ptr' will be false, even though they would have the same address, as ptr has provenance and ptr' does not.

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

If this pointer is at a null location, i.e. has no provenance

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

If these two pointers are at the same location (ie. same allocation)

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

The symbolic constraints needed for the pointer to be valid.

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

Generates a nondeterministic pointer, that is valid for accesses to the given type. The location of the pointer is nondeterministic; it could point to any allocation.

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

For Miri: the allocation ID of this location, as a u64

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

Returns a symbolic boolean to check whether this pointer has the given alignment, along with the error to raise otherwise.

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

Get the allocation info for this pointer: its size and alignment

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

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

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

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

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