Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 18 insertions, 6 deletions

diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index b975371c..0fb12180 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -12,7 +12,8 @@ open InterpreterPaths
     This function doesn't reorganize the context to make sure we can read
     the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first.
  *)
-val read_place : access_kind -> place -> (typed_value -> m_fun) -> m_fun
+val read_place :
+  Meta.meta -> access_kind -> place -> (typed_value -> m_fun) -> m_fun
 
 (** Auxiliary function.
 
@@ -31,7 +32,13 @@ val read_place : access_kind -> place -> (typed_value -> m_fun) -> m_fun
     primitively copyable and contain borrows.
  *)
 val access_rplace_reorganize_and_read :
-  config -> bool -> access_kind -> place -> (typed_value -> m_fun) -> m_fun
+  config ->
+  Meta.meta ->
+  bool ->
+  access_kind ->
+  place ->
+  (typed_value -> m_fun) ->
+  m_fun
 
 (** Evaluate an operand.
 
@@ -42,11 +49,12 @@ val access_rplace_reorganize_and_read :
     of the environment, before evaluating all the operands at once.
     Use {!eval_operands} instead.
  *)
-val eval_operand : config -> operand -> (typed_value -> m_fun) -> m_fun
+val eval_operand :
+  config -> Meta.meta -> operand -> (typed_value -> m_fun) -> m_fun
 
 (** Evaluate several operands at once. *)
 val eval_operands :
-  config -> operand list -> (typed_value list -> m_fun) -> m_fun
+  config -> Meta.meta -> operand list -> (typed_value list -> m_fun) -> m_fun
 
 (** Evaluate an rvalue which is not a global (globals are handled elsewhere).
 
@@ -56,7 +64,11 @@ val eval_operands :
     reads should have been eliminated from the AST.
  *)
 val eval_rvalue_not_global :
-  config -> rvalue -> ((typed_value, eval_error) result -> m_fun) -> m_fun
+  config ->
+  Meta.meta ->
+  rvalue ->
+  ((typed_value, eval_error) result -> m_fun) ->
+  m_fun
 
 (** Evaluate a fake read (update the context so that we can read a place) *)
-val eval_fake_read : config -> place -> cm_fun
+val eval_fake_read : config -> Meta.meta -> place -> cm_fun