summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
authorSon Ho2021-12-17 18:54:13 +0100
committerSon Ho2021-12-17 18:54:13 +0100
commitce7ad73cd819306fa68c23277b88c1ad571442f6 (patch)
tree6c8b937055be662d53e67cdaff0030f92f5ac6b1 /src/Interpreter.ml
parent49507d66422863f8cee48631f945e3dec3423569 (diff)
Update reborrow_shared
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml9
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