diff options
| author | Son Ho | 2022-01-26 10:04:52 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-26 10:04:52 +0100 |
| commit | 14833cb33792703bf87c7e7d933687f289886294 (patch) | |
| tree | b7c18f894854372dbd318f9b5dd3b6c54696aa7e /src/Invariants.ml | |
| parent | 144b660f7cfb8b65672f5872c05272a9caa0de78 (diff) | |
Add a meta-value in SharedBorrow to carry the shared value
Diffstat (limited to 'src/Invariants.ml')
| -rw-r--r-- | src/Invariants.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 6ebd3375..ee58a1a3 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -242,7 +242,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (* Register the loan *) let _ = match bc with - | V.SharedBorrow bid -> register_borrow Shared bid + | V.SharedBorrow (_, bid) -> register_borrow Shared bid | V.MutBorrow (bid, _) -> register_borrow Mut bid | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid in @@ -451,8 +451,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Bottom, _ -> (* Nothing to check *) () | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with - | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut - -> ( + | V.SharedBorrow (_, bid), T.Shared + | 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 |