diff options
| author | Son Ho | 2022-04-21 12:28:44 +0200 |
|---|---|---|
| committer | Son Ho | 2022-04-21 12:28:44 +0200 |
| commit | 029a12e25e1ee883ac98472f2e032b466d765307 (patch) | |
| tree | 8f1070dcae74c4fb527a239e444ae1fecfca48fd /src/InterpreterBorrows.ml | |
| parent | 66862a29cf023ca4d586479a9690dc4f61d8573c (diff) | |
Improve the generation of names for given back values
Diffstat (limited to 'src/InterpreterBorrows.ml')
| -rw-r--r-- | src/InterpreterBorrows.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 89dfb274..1905cf79 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -92,7 +92,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) method! visit_Borrow outer bc = match bc with - | SharedBorrow (_, l') | InactivatedMutBorrow l' -> + | SharedBorrow (_, l') | InactivatedMutBorrow (_, l') -> (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) @@ -730,7 +730,7 @@ 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_value config l tv ctx - | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow l') -> + | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow (_, l')) -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) |