From 69ee995af7a79e97232a3411e00c2bea5078563e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jan 2022 18:12:20 +0100
Subject: Update some comments

---
 src/InterpreterStatements.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 0100a9c6..23fe8d3b 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -32,7 +32,13 @@ let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx
   let ctx = write_place_unwrap config Write p nv ctx in
   ctx
 
-(** Assign a value to a given place *)
+(** Assign a value to a given place.
+
+    Note that this function first pushes the value to assign in a dummy variable,
+    then prepares the destination (by ending borrows, etc.) before popping the
+    dummy variable and putting in its destination (after having checked that
+    preparing the destination didn't introduce ⊥).
+ *)
 let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value)
     (p : E.place) : C.eval_ctx =
   (* Push the rvalue to a dummy variable, for bookkeeping *)
@@ -827,9 +833,6 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
         (* Pop the stack frame and retrieve the return value *)
         let ctx, ret_value = ctx_pop_frame config ctx in
 
-        (* TODO: there might be a problem because the return value
-         * if hanging in the air while we assign to place! *)
-
         (* Move the return value to its destination *)
         let ctx = assign_to_place config ctx ret_value dest in
 
-- 
cgit v1.2.3