Module Tree_block.Encoder

type nonrec rust_val = Sptr.t Rust_val.t
val encode : offset:Soteria_rust_lib.Typed.T.sint Typed.t -> rust_val -> Charon.Types.ty -> ((rust_val * Soteria_rust_lib.Typed.T.sint Typed.t) Soteria.Soteria_std.Iter.t, [> `InvalidLayout of Charon.Types.ty ], 'f) Rustsymex.Result.t
val validity : ?check_ref: ((Sptr.t * (Soteria_rust_lib.Typed.T.sint Typed.t, Sptr.t) Rust_val.meta_raw) -> Charon.Types.ty -> (unit, [> `InvalidLayout of Charon.Types.ty ] as 'a, 'b) Rustsymex.Result.t) -> Charon.Types.ty -> (Soteria_rust_lib.Typed.T.sint Typed.t, Soteria_rust_lib.Typed.T.sfloat Typed.t, Sptr.t) Rust_val.raw -> ([> Typed.sbool ] Typed.t -> Error.t -> (unit, 'a, 'b) Rustsymex.Result.t) -> (unit, 'a, 'b) Rustsymex.Result.t
val check_validity : check_ref: ((Sptr.t * (Soteria_rust_lib.Typed.T.sint Typed.t, Sptr.t) Rust_val.meta_raw) -> Charon.Types.ty -> 'a -> Soteria_rust_lib__Rustsymex.MonadState.t -> (((unit, Error.t, 'b) Soteria.Symex.Compo_res.t * 'c) * Soteria_rust_lib__Rustsymex.MonadState.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) -> Charon.Types.ty -> (Soteria_rust_lib.Typed.T.sint Typed.t, Soteria_rust_lib.Typed.T.sfloat Typed.t, Sptr.t) Rust_val.raw -> 'a -> Soteria_rust_lib__Rustsymex.MonadState.t -> (((unit, Error.t, 'b) Soteria.Symex.Compo_res.t * 'a) * Soteria_rust_lib__Rustsymex.MonadState.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t
val cast_literal : from_ty:Charon.Types.literal_type -> to_ty:Charon.Types.literal_type -> [< Soteria_rust_lib.Typed.T.cval ] Typed.t -> ([< Soteria_rust_lib.Typed.T.any NonZero Zero ] Typed.t, [> Soteria__Bv_values__Typed.T.sfloat ] Typed.t, 'a) Rust_val.raw
val float_to_bv_bits : [< Soteria__Bv_values__Typed.T.sfloat ] Typed.t -> [ `NonZero | `Zero ] Typed.t Sptr.DecayMapMonad.t
val transmute_one : to_ty:Charon.Types.ty -> rust_val -> rust_val Sptr.DecayMapMonad.t
val nondet_raw : Charon.Types.ty -> (rust_val, [> Error.t ], 'f) Rustsymex.Result.t
val nondet_valid : Charon.Types.ty -> Soteria_rust_lib__Rustsymex.MonadState.t -> ((rust_val, [> Error.t ], 'a) Soteria.Symex.Compo_res.t * Soteria_rust_lib__Rustsymex.MonadState.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t
val apply_attribute : ([< Soteria__Bv_values__Typed.T.sint ] Typed.t, 'a, 'b) Rust_val.raw -> Charon.Meta.attribute -> Soteria_rust_lib__Rustsymex.MonadState.t -> ((unit, [> `StdErr of string ], 'c) Soteria.Symex.Compo_res.t * Soteria_rust_lib__Rustsymex.MonadState.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t
val apply_attributes : ([< Soteria__Bv_values__Typed.T.sint ] Typed.t, 'a, 'b) Rust_val.raw -> Charon.Meta.attribute list -> (unit, [> `StdErr of string ], 'c) Rustsymex.Result.t
val ref_tys_in : ?include_ptrs:bool -> rust_val -> Charon.Types.ty -> (Sptr.t Rust_val.full_ptr * Charon.Types.ty) Soteria.Soteria_std.List.t
val update_ref_tys_in : ('acc -> Sptr.t Rust_val.full_ptr -> Charon.Types.ty -> (Sptr.t Rust_val.full_ptr * 'acc, 'e, 'f) Rustsymex.Result.t) -> 'acc -> rust_val -> Charon.Types.ty -> (rust_val * 'acc, 'e, 'f) Rustsymex.Result.t
val size_and_align_of_val : load: ((Sptr.t * ('a, 'b) Rust_val.meta_raw) -> Charon.Types.ty_kind -> 'c -> Soteria_rust_lib__Rustsymex.MonadState.t -> (((([< Soteria_rust_lib.Typed.T.any ] Typed.t, 'd Typed.t, 'e) Rust_val.raw, [> Error.t ] as 'f, 'g) Soteria.Symex.Compo_res.t * 'h) * Soteria_rust_lib__Rustsymex.MonadState.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) -> t:Charon.Types.ty -> meta:([< Soteria_rust_lib.Typed.T.any ] Typed.t, Sptr.t) Rust_val.meta_raw -> 'c -> Soteria_rust_lib__Rustsymex.MonadState.t -> ((Soteria_rust_lib.Typed.T.sint Typed.t * Soteria_rust_lib.Typed.T.nonzero Typed.t, 'f, 'g) Soteria.Symex.Compo_res.t * Soteria_rust_lib__Rustsymex.MonadState.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t