diff options
author | Son Ho | 2022-01-06 16:58:46 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 16:58:46 +0100 |
commit | 808f21c06314ccbbe2a61835899c943b532c9783 (patch) | |
tree | fd26f8d1c5649fe77a4de6bc7d508e7bdd5ad010 | |
parent | 335de855331a424c35b577907eb504c198990c0b (diff) |
Implement a small improvement for apply_reborrows
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterProjectors.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index dfc821de..ada1a89a 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -430,13 +430,20 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) functions) on purpose: exhaustive matches are good for maintenance *) method! visit_aloan_content env lc = - (* TODO: ashared_loan (amut_loan ) case *) match lc with - | V.ASharedLoan (bids, v, av) -> + | V.ASharedLoan (bids, sv, av) -> (* Insert the reborrows *) let bids = insert_reborrows bids in + (* Similarly to the non-abstraction case: check if the shared + * value is a mutable borrow, to eventually insert more reborrows *) (* Update and explore *) - super#visit_ASharedLoan env bids v av + let bids = + match get_borrow_in_mut_borrow sv with + | None -> bids + | Some bid -> insert_reborrows_for_bid bids bid + in + (* Update and explore *) + super#visit_ASharedLoan env bids sv av | V.AIgnoredSharedLoan _ | V.AMutLoan (_, _) | V.AEndedMutLoan { given_back = _; child = _ } |