summaryrefslogtreecommitdiff
path: root/src/InterpreterProjectors.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterProjectors.ml8
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