Interp (soteria-rust.Soteria_rust_lib.Analyses.Wpst.Interp)

module StateM : sig ... end

module Core : sig ... end

module Std_funs : sig ... end

exception Unsupported of string * Charon.Meta.span_data

type 'a t = ('a, StateM.Sptr.t Store.t) StateM.t

type 'err fun_exec = StateM.rust_val list -> (StateM.rust_val, unit) StateM.t

type lazy_ptr =

| Store of Charon.Expressions.local_id
| Heap of StateM.full_ptr

val pp_lazy_ptr : 
  Ppx_deriving_runtime.Format.formatter ->
  lazy_ptr ->
  Ppx_deriving_runtime.unit

val show_lazy_ptr : lazy_ptr -> Ppx_deriving_runtime.string

val get_variable_ptr : 
  Store.Map.key ->
  (StateM.Sptr.t Rust_val.full_ptr, StateM.Sptr.t Store.t) StateM.t

val get_variable_lazy : 
  Store.Map.key ->
  (lazy_ptr, StateM.Sptr.t Store.t) StateM.t

val get_variable_lazy_and_ty : 
  Store.Map.key ->
  (lazy_ptr * Charon.Types.ty, StateM.Sptr.t Store.t) StateM.t

val load_lazy : lazy_ptr -> Charon.Types.ty -> StateM.rust_val t

val store_lazy : 
  lazy_ptr ->
  Charon.Types.ty ->
  StateM.Sptr.t Rust_val.t ->
  unit t

val uninit_lazy : lazy_ptr -> Charon.Types.ty -> unit t

val alloc_stack : 
  Charon.GAst.locals ->
  StateM.rust_val list ->
  ((StateM.full_ptr * Charon.Types.ty) list,
    StateM.Sptr.t Store.binding Store.Map.t)
    StateM.t

val dealloc_stack : 
  ?protected_address:StateM.Sptr.t ->
  (StateM.full_ptr * Charon.Types.ty) list ->
  (unit, StateM.Sptr.t Store.t) StateM.t

val resolve_fn_ptr : Charon.Types.fn_ptr -> Common.Fun_kind.t t

val resolve_constant : 
  Charon.Types.constant_expr ->
  ((Soteria_rust_lib.Typed.T.sint Soteria.Bv_values.Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    StateM.Sptr.t Store.t)
    StateM.t

val resolve_place : Charon.Expressions.place -> StateM.full_ptr t

val resolve_place_lazy : Charon.Expressions.place -> lazy_ptr t

val resolve_function : 
  in_tys:Charon.Types.ty list ->
  out_ty:Charon.Types.ty ->
  Charon.GAst.fn_operand ->
  ('a fun_exec * Charon.Types.ty Soteria.Soteria_std.List.t) t

val resolve_global : 
  Charon.Types.global_decl_ref ->
  (StateM.full_ptr, StateM.Sptr.t Store.t) StateM.t

val eval_operand : 
  Charon.Expressions.operand ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    StateM.Sptr.t Store.t)
    StateM.t

val eval_operand_list : 
  Charon.Expressions.operand list ->
  ((Soteria_rust_lib.Typed.T.sint Soteria.Bv_values.Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw
     list,
    StateM.Sptr.t Store.t)
    StateM.t

val eval_rvalue : 
  Charon.Expressions.rvalue ->
  Charon.Types.ty ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    StateM.Sptr.t Store.t)
    StateM.t

val exec_stmt : 
  Charon.UllbcAst.statement ->
  (unit, StateM.Sptr.t Store.t) StateM.t

val exec_block : 
  body:Charon.UllbcAst.expr_body ->
  Charon.UllbcAst.block ->
  (StateM.rust_val, StateM.Sptr.t Store.t) StateM.t

val exec_real_fun : 
  Charon.UllbcAst.fun_decl ->
  Charon.Types.generic_args ->
  'a fun_exec

val exec_fun : 
  args:StateM.rust_val list ->
  state:StateM.st ->
  Charon.UllbcAst.fun_decl ->
  (StateM.rust_val * StateM.st, Error.with_trace * StateM.st, StateM.syn list)
    Soteria.Symex.Compo_res.t
    Rustsymex.t