diff options
| author | Son Ho | 2022-01-27 11:43:59 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-27 11:43:59 +0100 |
| commit | b2d5671516b60ae83778b26867a8e5b6060f519d (patch) | |
| tree | 90aefb82bb32da8671a54543300a0a1155c2d8d7 /src/InterpreterBorrowsCore.ml | |
| parent | 98677400fc27087ab4443094fb94a95412515422 (diff) | |
Introduce AEndedSharedBorrow so as not to introduce ABottom when
ending shared aborrows
Diffstat (limited to 'src/InterpreterBorrowsCore.ml')
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index b4ab7706..941ac140 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -434,7 +434,8 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.AIgnoredMutBorrow (_, _) | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow - { given_back_loans_proj = _; child = _; given_back_meta = _ } -> + { given_back_loans_proj = _; child = _; given_back_meta = _ } + | V.AEndedSharedBorrow -> super#visit_aborrow_content env bc | V.AProjSharedBorrow asb -> if borrow_in_asb l asb then @@ -548,7 +549,7 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) | V.ASharedBorrow bid -> if bid = l then update () else V.ABorrow (super#visit_ASharedBorrow env bid) - | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ + | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedSharedBorrow | V.AEndedIgnoredMutBorrow _ -> super#visit_ABorrow env bc | V.AProjSharedBorrow asb -> |