Sptr (soteria-rust.Soteria_rust

module type DecayMapS = sig ... end

A map to store information on "decayed" pointers, namely mapping from locations to integers (their decayed) value.

module DecayMap : DecayMapS

module DecayMapMonad : sig ... end

module D_abstr : sig ... end

module type S = sig ... end

type ('sptr, 'snonzero, 'sint) arithptr = {

ptr : 'sptr;
tag : Tree_borrow.tag option;
align : 'snonzero;
size : 'sint;

}

module ArithPtr : 
  S
    with type t =
           (Soteria_rust_lib.Typed.T.sptr Typed.t,
             Soteria_rust_lib.Typed.T.nonzero Typed.t,
             Soteria_rust_lib.Typed.T.sint Typed.t)
             arithptr
     and type syn =
           (Soteria_rust_lib.Typed.Expr.t,
             Soteria_rust_lib.Typed.Expr.t,
             Soteria_rust_lib.Typed.Expr.t)
             arithptr

A pointer that can perform pointer arithmetics -- all pointers are a pair of location and offset, along with an optional metadata.