Session (soteria-rust.Soteria_rust_lib.Interp.Make.StateM.Layout.Session)

type cache = (Charon.Types.ty, t) Soteria.Soteria_std.Hashtbl.t

type Stdlib.Effect.t +=

| Get_cache : cache Stdlib.Effect.t

val get_cache : unit -> cache

val with_layout_cache : (unit -> 'a) -> 'a

val get_or_compute_cached_layout : 
  Charon.Types.ty ->
  (unit ->
    Soteria_rust_lib__Rustsymex.MonadState.t ->
    ((t, 'a, 'b) Soteria.Symex.Compo_res.t
     * Soteria_rust_lib__Rustsymex.MonadState.t)
      Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t) ->
  (t, 'a, 'b) Rustsymex.Result.t