diff options
author | Son Ho | 2022-01-06 16:24:40 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 16:24:40 +0100 |
commit | b83b928109b528c02e16df099c6f9b132e920b12 (patch) | |
tree | 23bffc6578c4f67c512f3089565b7903908ce6c2 /src/InterpreterBorrows.ml | |
parent | 407474a35b7dd80116c8d358873d25e1a9b49048 (diff) |
Fix more bugs
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterBorrows.ml | 10 |
1 files changed, 8 insertions, 2 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) |