Encoder (soteria-rust.Soteria_rust_lib.State.Tree

type nonrec rust_val = Sptr.t Rust_val.t

val pp_rust_val : 
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    Sptr.t)
    Rust_val.raw
    Fmt.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