Module Layout_common.Fields_shape

We use a custom type for the member offsets for layouts; this allows us to use a more efficient representation for arrays T; N, that doesn't require N offsets.

type t =
  1. | Primitive
    (*

    No fields present

    *)
  2. | Arbitrary of Charon.Types.variant_id * Soteria_rust_lib.Typed.T.sint Typed.t Stdlib.Array.t
    (*

    Arbitrary field placement (structs, unions...), with the variant (e.g. enums with a single inhabited variant)

    *)
  3. | Enum of Tag_layout.t * t Stdlib.Array.t
    (*

    Enum fields: encodes a tag, and an array of field shapes for each variant (indexed by variant ID). Using offset_of on this isn't valid; one must first retrieve the fields shape of the corresponding variant.

    *)
  4. | Array of Soteria_rust_lib.Typed.T.sint Typed.t
    (*

    All fields are equally spaced (arrays, slices)

    *)
val pp : t Fmt.t
val offset_of : int -> t -> Soteria_rust_lib.Typed.T.sint Typed.t
val shape_for_variant : Charon.Types.VariantId.id -> t -> t
val iter_vars : t -> ((Soteria.Symex.Var.t * 'a Typed.ty) -> unit) -> unit