From b2d5671516b60ae83778b26867a8e5b6060f519d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 11:43:59 +0100
Subject: Introduce AEndedSharedBorrow so as not to introduce ABottom when
 ending shared aborrows

---
 src/Invariants.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 522f2ffa..fe1b5e82 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -257,7 +257,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
           | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
           | V.AIgnoredMutBorrow (None, _)
           | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _
-          | V.AProjSharedBorrow _ ->
+          | V.AEndedSharedBorrow | V.AProjSharedBorrow _ ->
               (* Do nothing *)
               ()
         in
@@ -361,7 +361,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
         let info =
           match bc with
           | V.AMutBorrow (_, _, _) -> set_outer_mut info
-          | V.ASharedBorrow _ -> set_outer_shared info
+          | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info
           | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
           | V.AEndedIgnoredMutBorrow _ ->
               set_outer_mut info
-- 
cgit v1.2.3