diff options
| author | Son Ho | 2021-12-17 18:55:06 +0100 |
|---|---|---|
| committer | Son Ho | 2021-12-17 18:55:06 +0100 |
| commit | 7bd3b03e28ac8591aad130b52376f0827af69e91 (patch) | |
| tree | 09039bc0202bad7d7e2310f27efa9ece26240060 /src/Interpreter.ml | |
| parent | ce7ad73cd819306fa68c23277b88c1ad571442f6 (diff) | |
Update give_back
Diffstat (limited to 'src/Interpreter.ml')
| -rw-r--r-- | src/Interpreter.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index cb883768..3101ebaf 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1507,7 +1507,11 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_shared config l ctx - | Abstract (V.AIgnoredSharedBorrow _) -> raise Unimplemented + | Abstract (V.AIgnoredSharedBorrow asb) -> + (* Sanity check *) + assert (borrow_in_asb l asb); + (* Update the context *) + give_back_shared config l ctx | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable" (** End a borrow identified by its borrow id in a context |