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/Invariants.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 6ebd3375..ee58a1a3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -242,7 +242,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
         (* Register the loan *)
         let _ =
           match bc with
-          | V.SharedBorrow bid -> register_borrow Shared bid
+          | V.SharedBorrow (_, bid) -> register_borrow Shared bid
           | V.MutBorrow (bid, _) -> register_borrow Mut bid
           | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid
         in
@@ -451,8 +451,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Bottom, _ -> (* Nothing to check *) ()
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
             match (bc, rkind) with
-            | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
-              -> (
+            | V.SharedBorrow (_, bid), T.Shared
+            | V.InactivatedMutBorrow bid, T.Mut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
                 let _, glc = lookup_loan ek_all bid ctx in
                 match glc with
-- 
cgit v1.2.3