diff options
Diffstat (limited to 'src/InterpreterProjectors.ml')
-rw-r--r-- | src/InterpreterProjectors.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 946bacea..76b7d6ae 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -56,7 +56,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) bv ref_ty in (bid, asb) - | V.SharedBorrow bid, T.Shared -> + | V.SharedBorrow (_, bid), T.Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in @@ -172,7 +172,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) fresh_reborrow regions ancestors_regions bv ref_ty in V.AMutBorrow (mv, bid, bv) - | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid + | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid | V.InactivatedMutBorrow _, _ -> failwith "Can't apply a proj_borrow over an inactivated mutable \ @@ -197,7 +197,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) in (* Return *) V.AIgnoredMutBorrow (opt_bid, bv) - | V.SharedBorrow bid, T.Shared -> + | V.SharedBorrow (_, bid), T.Shared -> (* Lookup the shared value *) let ek = ek_all in let sv = lookup_loan ek bid ctx in @@ -370,7 +370,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) match v.V.value with | V.Borrow lc -> ( match lc with - | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None + | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> None | V.MutBorrow (id, _) -> Some id) | _ -> None in |