From ed1562db8a72631e36b89171b377e395cb0f8632 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 17 Dec 2021 10:24:00 +0100
Subject: Make minor modifications

---
 src/Interpreter.ml | 12 ++++++++++++
 src/Values.ml      |  2 ++
 2 files changed, 14 insertions(+)

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 4ea95028..8948701f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -846,6 +846,18 @@ let give_back_shared_to_abs _config _bid _abs : V.abs =
  *)
 let give_back_value (config : C.config) (bid : V.BorrowId.id)
     (v : V.typed_value) (env : C.env) : C.env =
+  (* TODO:
+     (* We use a reference to check that we updated exactly one borrow *)
+     let replaced : bool ref = ref false in
+     let set_replaced () =
+       assert (not !replaced);
+       replaced := true
+     in
+     let obj =
+       object
+         inherit [_] C.map_env
+       end
+        in*)
   let give_back_value_to_env_elem ev : C.env_elem =
     match ev with
     | C.Var (vid, destv) ->
diff --git a/src/Values.ml b/src/Values.ml
index 8c4c689c..3905d96e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -241,6 +241,8 @@ and aloan_content =
     note independent of the parent avalues. For instance, a value
     `AMutBorrow (_, AMutBorrow (_, ...)` (ignoring the types) really is
     to be seen like a `mut_borrow ... (mut_borrow ...)`.
+    
+    TODO: be more precise about the ignored vlaues
 *)
 and aborrow_content =
   | AMutBorrow of (BorrowId.id[@opaque]) * typed_avalue
-- 
cgit v1.2.3