From 14833cb33792703bf87c7e7d933687f289886294 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 10:04:52 +0100
Subject: Add a meta-value in SharedBorrow to carry the shared value

---
 src/InterpreterBorrowsCore.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'src/InterpreterBorrowsCore.ml')

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 81f9d0d3..b4ab7706 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -194,9 +194,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_borrow_content env bc =
         match bc with
-        | V.SharedBorrow bid ->
+        | V.SharedBorrow (mv, bid) ->
             (* Nothing specific to do *)
-            super#visit_SharedBorrow env bid
+            super#visit_SharedBorrow env mv bid
         | V.InactivatedMutBorrow bid ->
             (* Nothing specific to do *)
             super#visit_InactivatedMutBorrow env bid
@@ -305,7 +305,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
 
       method! visit_borrow_content env bc =
         match bc with
-        | V.SharedBorrow _ | V.InactivatedMutBorrow _ ->
+        | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ ->
             (* Nothing specific to do *)
             super#visit_borrow_content env bc
         | V.MutBorrow (bid, mv) ->
@@ -407,7 +407,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
             if bid = l then raise (FoundGBorrowContent (Concrete bc))
             else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
             else ()
-        | V.SharedBorrow bid ->
+        | V.SharedBorrow (_, bid) ->
             (* Check the borrow id *)
             if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
         | V.InactivatedMutBorrow bid ->
@@ -490,9 +490,9 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
             if bid = l then update ()
             else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
             else V.MutBorrow (bid, mv)
-        | V.SharedBorrow bid ->
+        | V.SharedBorrow (mv, bid) ->
             (* Check the id *)
-            if bid = l then update () else super#visit_SharedBorrow env bid
+            if bid = l then update () else super#visit_SharedBorrow env mv bid
         | V.InactivatedMutBorrow bid ->
             (* Check the id *)
             if bid = l then update ()
-- 
cgit v1.2.3