Value_codec (soteria-rust.Soteria_rust_lib.Value

module Compo_res = Soteria.Symex.Compo_res

module DecayMapMonad = Sptr.DecayMapMonad

val variant_for_discr : 
  [< Soteria__Bv_values__Typed.T.any ] Soteria__Bv_values__Typed.t ->
  Charon.Types.type_decl_ref ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((Charon.Types.VariantId.id * Charon.Types.variant)
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

Returns the variant id and variant matching the given discriminant.

val iter_fields : 
  ?variant:Charon.Types.VariantId.id ->
  ?meta:
    ([< Soteria__Bv_values__Typed.T.any ] Soteria__Bv_values__Typed.t, 'a)
      Rust_val.meta_raw ->
  Layout.t ->
  Charon.Types.ty ->
  (Charon.Types.ty * Soteria_rust_lib.Typed.T.sint Typed.t)
    Soteria.Soteria_std.Iter.t

Iterator over the fields and offsets of a type; for primitive types, returns a singleton iterator for that value.

val size_of : 
  ([< Soteria_rust_lib.Typed.T.sint ] Typed.t,
    [< Soteria__Bv_values__Typed.T.sfloat ] Soteria__Bv_values__Typed.t,
    'a)
    Rust_val.raw ->
  ([> Soteria__Bv_values__Typed.T.sint ] Typed.t,
    [> `InvalidLayout of Charon.Types.ty ],
    'b)
    Rustsymex.Result.t

module Decoder (Sptr : Sptr.S) (State_tys : sig ... end) : sig ... end

module Encoder (Sptr : Sptr.S) : sig ... end