diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterPaths.ml | 29 |
1 files changed, 8 insertions, 21 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index f0fb3333..d8b1322b 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -606,38 +606,25 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) * a recursive call to reinspect the value *) comp cc (end_loans_at_place config access p) cf ctx) -(** Drop (end) loans and borrows at a given place, which should be +(** Drop (end) outer loans and borrows at a given place, which should be seen as an l-value (we will write to it later, but need to drop the borrows before writing). - This is used to drop values (when we need to write to a place, we first - drop the value there to properly propagate back values which are not/can't - be borrowed anymore). + This is used to drop values when evaluating the drop statement or before + writing to a place. [end_borrows]: - - if true: end all the loans and borrows we find. This is used for instance - by [drop_value]. + - if true: end all the loans and borrows we find, starting with the outer + ones. This is used when evaluating the `drop` statement (see [drop_value]) - if false: only end the outer loans. This is used by [assign_to_place] or to drop the loans in the local variables when popping a frame. Note that we don't do what is defined in the formalization: we move the value to a temporary dummy value, then explore this value and end the loans/borrows inside as long as we find some, starting with the outer - ones. - - TODO: rewrite that. Consider the following example: - Example: - ======= - We want to end the borrows/loans at `*x` in the following environment: - ``` - x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), - mut_loan l2, mut_borrow l2 (mut_loan l3)) - y -> mut_borrow l3 (Bool true) - ``` - We have to consider several things: - - the borrows `mut_borrow l1 (Int 3)` `mut_borrow l2 ...` borrow subvalues of `*x` - - we can't immediately end `mut_borrow l2 ...` because it contains a loan - - the borrow corresponding to the loan `mut_loan l3` is outside of `*x` + ones, then move the resulting value back to where it was. This shouldn't + make any difference, really (note that the place is *inside* a borrow, + if we end the borrow, we won't be able to reinsert the value back). *) let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) (p : E.place) : cm_fun = |