diff options
| -rw-r--r-- | src/InterpreterBorrows.ml | 10 | ||||
| -rw-r--r-- | src/Invariants.ml | 11 |
2 files changed, 14 insertions, 7 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index ca1f87f1..fbd958ef 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -5,6 +5,7 @@ module Subst = Substitute module L = Logging open Utils open ValuesUtils +open TypesUtils open InterpreterUtils open InterpreterBorrowsCore open InterpreterProjectors @@ -265,6 +266,11 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) | None -> failwith "Unreachable" | Some abs -> abs.V.regions in + (* Rk.: there is a small issue with the types of the aloan values *) + let borrowed_value_aty = + let _, ty, _ = ty_get_ref ty in + ty + in match lc with | V.AMutLoan (bid', child) -> if bid' = bid then ( @@ -276,7 +282,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* Apply the projection *) let given_back = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions nv ty + regions nv borrowed_value_aty in (* Return the new value *) V.ALoan (V.AEndedMutLoan { given_back; child })) @@ -302,7 +308,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) * (i.e., we don't call [set_replaced]) *) let given_back = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions nv ty + regions nv borrowed_value_aty in V.ALoan (V.AEndedIgnoredMutLoan { given_back; child }) else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) diff --git a/src/Invariants.ml b/src/Invariants.ml index b723d861..11b00381 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -523,14 +523,15 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> failwith "Inconsistent context") | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av) -> - let ty = Subst.erase_regions aty in - assert (sv.V.ty = ty); + let borrowed_aty = aloan_get_expected_child_type aty in + assert (sv.V.ty = Subst.erase_regions borrowed_aty); (* TODO: the type of aloans doesn't make sense, see above *) - assert (child_av.V.ty = aloan_get_expected_child_type aty) + assert (child_av.V.ty = borrowed_aty) | V.AEndedMutLoan { given_back; child } | V.AEndedIgnoredMutLoan { given_back; child } -> - assert (given_back.V.ty = aloan_get_expected_child_type aty); - assert (child.V.ty = aloan_get_expected_child_type aty) + let borrowed_aty = aloan_get_expected_child_type aty in + assert (given_back.V.ty = borrowed_aty); + assert (child.V.ty = borrowed_aty) | V.AIgnoredSharedLoan child_av -> assert (child_av.V.ty = aloan_get_expected_child_type aty)) | V.ASymbolic aproj, ty -> |