M (soteria-rust.Soteria_rust_lib.Builtins.Eval.M)

Parameters

module StateM : State.StateM.S

Signature

module Alloc : sig ... end

module Intrinsics : sig ... end

module Miri : sig ... end

module Soteria_lib : sig ... end

module Std : sig ... end

module System : sig ... end

val fn_to_stub : 
  Charon.Types.fun_sig ->
  Charon.Types.name ->
  (Common.Fun_kind.t ->
    (Soteria_rust_lib.Typed.T.sint Typed.t,
      Soteria_rust_lib.Typed.T.sfloat Typed.t,
      StateM.Sptr.t)
      Rust_val.raw
      list ->
    ('a, unit) StateM.t) ->
  fn ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    StateM.Sptr.t)
    Rust_val.raw
    list ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    'b)
    StateM.t

val std_fun_eval : 
  Charon.UllbcAst.fun_decl ->
  Charon.Types.generic_args ->
  (Common.Fun_kind.t ->
    (Soteria_rust_lib.Typed.T.sint Typed.t,
      Soteria_rust_lib.Typed.T.sfloat Typed.t,
      StateM.Sptr.t)
      Rust_val.raw
      list ->
    (StateM.Sptr.t Rust_val.t, unit) StateM.t) ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    StateM.Sptr.t)
    Rust_val.raw
    list ->
  (StateM.Sptr.t Rust_val.t, unit) StateM.t