diff options
author | Son Ho | 2021-12-17 18:54:13 +0100 |
---|---|---|
committer | Son Ho | 2021-12-17 18:54:13 +0100 |
commit | ce7ad73cd819306fa68c23277b88c1ad571442f6 (patch) | |
tree | 6c8b937055be662d53e67cdaff0030f92f5ac6b1 | |
parent | 49507d66422863f8cee48631f945e3dec3423569 (diff) |
Update reborrow_shared
-rw-r--r-- | src/Interpreter.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 90638d96..cb883768 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1455,7 +1455,14 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) V.ASharedLoan (bids', v, av)) else super#visit_ASharedLoan env bids v av - method! visit_AIgnoredSharedLoan _ _ = raise Unimplemented + method! visit_AIgnoredSharedLoan env asb = + (* Check if the set of abstract shared borrows contains the borrow + * we want to duplicate *) + if borrow_in_asb original_bid asb then ( + set_ref (); + let asb = V.AsbBorrow new_bid :: asb in + V.AIgnoredSharedLoan asb) + else super#visit_AIgnoredSharedLoan env asb end in |