Module Soteria_rust_lib.Rust_val

type ('v, 'ptr) meta_raw =
  1. | Thin
  2. | Len of 'v
  3. | VTable of 'ptr
type 'ptr meta_syn = (Soteria_rust_lib.Typed.Expr.t, 'ptr) meta_raw
type ('v, 'ptr) full_ptr_raw = 'ptr * ('v, 'ptr) meta_raw
type 'ptr full_ptr = 'ptr * 'ptr meta
type ('sint, 'sfloat, 'ptr) raw =
  1. | Int of 'sint
  2. | Float of 'sfloat
  3. | Ptr of ('sint, 'ptr) full_ptr_raw
    (*

    pointer, parametric to enable Ruxt, with optional meta

    *)
  4. | Enum of 'sint * ('sint, 'sfloat, 'ptr) raw list
    (*

    discriminant * values

    *)
  5. | Tuple of ('sint, 'sfloat, 'ptr) raw list
    (*

    contains ordered values

    *)
  6. | Union of (('sint, 'sfloat, 'ptr) raw * 'sint) list
    (*

    list of blocks in the union, with their offset

    *)
  7. | PolyVal of Charon.Types.type_var_id
    (*

    The opaque value of a type variable, identified by (type variable index, unique identifier).

    *)
type 'ptr rust_val = 'ptr t
val pp_meta_raw : (Stdlib.Format.formatter -> 'a -> unit) -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.Format.formatter -> ('a, 'b) meta_raw -> unit
val pp_meta : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> ('b Typed.t, 'a) meta_raw -> unit
val pp_meta_syn : (Stdlib.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Stdlib.Format.formatter -> (Soteria_rust_lib.Typed.Expr.t, 'a) meta_raw -> Ppx_deriving_runtime.unit
val pp_full_ptr_raw : (Stdlib.Format.formatter -> 'a -> unit) -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.Format.formatter -> ('b * ('a, 'b) meta_raw) -> unit
val pp_full_ptr : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> ('a * ('b Typed.t, 'a) meta_raw) -> unit
val pp_full_ptr_syn : (Stdlib.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Stdlib.Format.formatter -> ('a * (Soteria_rust_lib.Typed.Expr.t, 'a) meta_raw) -> Ppx_deriving_runtime.unit
val pp : (Stdlib.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> ('b Typed.t, 'c Typed.t, 'a) raw Fmt.t
val pp_rust_val : (Stdlib.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> ('b Typed.t, 'c Typed.t, 'a) raw Fmt.t
val pp_syn : (Stdlib.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, 'a) raw Fmt.t
val ppa_syn : Stdlib.Format.formatter -> (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, 'a) raw -> unit
val ppa : Stdlib.Format.formatter -> ('a Typed.t, 'b Typed.t, 'c) raw -> unit
val unit_ : ('a, 'b, 'c) raw
val meta_exprs_syn : ('ptr -> Soteria_rust_lib.Typed.Expr.t list) -> 'ptr meta_syn -> Soteria_rust_lib.Typed.Expr.t list
val to_syn : ('ptr -> 'a) -> (Soteria_rust_lib.Typed.T.sint Typed.t, 'b Soteria__Bv_values__Typed.t, 'ptr) raw -> (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, 'a) raw
module Learn_eq (Symex : Soteria.Symex.Base with module Value = Typed) : sig ... end
val is_empty : ('a, 'b, 'c) raw -> bool

is_empty v is true if the value is "empty"; ie. it doesn't contain any Base or Ptr value. We also consider Enum to be non-empty, because of the discriminant, though this *may* be wrong if it's a ZST.

Used in unsizing, to find the field with the pointer to modify.

val as_ptr : ('a Typed.t, 'b Typed.t, 'c) raw -> ('a Typed.t, 'c) full_ptr_raw
val as_ptr_or : make:([< Soteria_rust_lib.Typed.T.any NonZero Zero ] Typed.t -> 'a) -> (([< Soteria_rust_lib.Typed.T.any ] as 'b) Typed.t, 'c Typed.t, 'a) raw -> ('b Typed.t, 'a) full_ptr_raw
val as_base_f : Charon.Types.float_type -> ('a Typed.t, [< Soteria_rust_lib.Typed.T.any ] Typed.t, 'b) raw -> Soteria_rust_lib.Typed.T.sfloat Typed.t
val as_base : Charon.Types.literal_type -> ([< Soteria_rust_lib.Typed.T.any ] Typed.t, 'a Typed.t, 'b) raw -> [< Soteria_rust_lib.Typed.T.any NonZero Zero ] Typed.t
val as_base_i : Charon.Values.u_int_ty -> ([< Soteria_rust_lib.Typed.T.any ] Typed.t, 'a Typed.t, 'b) raw -> [< Soteria_rust_lib.Typed.T.any NonZero Zero ] Typed.t
val as_tuple : ('a Typed.t, 'b Typed.t, 'c) raw -> ('a Typed.t, 'b Typed.t, 'c) raw list
val flatten : ('a, 'b, 'c) raw -> ('a, 'b, 'c) raw list
val subst : ((Soteria_rust_lib.Typed.Expr.t -> 'a Soteria__Bv_values__Typed.t) -> 'b -> 'c) -> (Soteria_rust_lib.Typed.Expr.t -> 'a Soteria__Bv_values__Typed.t) -> (Soteria_rust_lib.Typed.Expr.t, Soteria_rust_lib.Typed.Expr.t, 'b) raw -> ('d Soteria__Bv_values__Typed.t, 'e Soteria__Bv_values__Typed.t, 'c) raw