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/Invariants.ml | |
| parent | 66862a29cf023ca4d586479a9690dc4f61d8573c (diff) | |
Improve the generation of names for given back values
Diffstat (limited to '')
| -rw-r--r-- | src/Invariants.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index f12911d4..81e35de3 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -244,7 +244,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match bc with | V.SharedBorrow (_, bid) -> register_borrow Shared bid | V.MutBorrow (bid, _) -> register_borrow Mut bid - | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid + | V.InactivatedMutBorrow (_, bid) -> register_borrow Inactivated bid in (* Continue exploring *) super#visit_borrow_content env bc @@ -461,7 +461,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with | V.SharedBorrow (_, bid), T.Shared - | V.InactivatedMutBorrow bid, T.Mut -> ( + | V.InactivatedMutBorrow (_, bid), T.Mut -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan ek_all bid ctx in match glc with |