summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-14 10:49:15 +0100
committerSon Ho2021-12-14 10:49:15 +0100
commit6f02817f52786ee6a9aedfcb3460466d5cf6cff5 (patch)
tree721ec600fb575578fe1611c719d7175e2c059624 /src
parent5391ca0c4dbb745044a2920dbd7dac70d251e670 (diff)
Make minor modifications
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml13
1 files changed, 10 insertions, 3 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index e0ded437..4b2a303c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -908,11 +908,15 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer)
* we shouldn't need to end outer borrows if io=Inner, so we just
* add the following assertion *)
assert (io = Outer);
+ (* Note that we might get there with `allowed_abs <> None`: we might
+ * be trying to end a borrow inside an abstraction, but which is actually
+ * inside another borrow *)
let allowed_abs' = None in
let env = end_borrows_in_env config io allowed_abs' bids env in
(* Retry to end the borrow *)
end_borrow_in_env config io allowed_abs l env
| OuterBorrows (Borrow bid) ->
+ (* See the comments for the previous case *)
assert (io = Outer);
let allowed_abs' = None in
let env = end_borrow_in_env config io allowed_abs' bid env in
@@ -923,6 +927,7 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer)
* loan is inside the same abstraction. If this is the case, we end
* the borrow without ending the abstraction. If not, we need to
* end the whole abstraction *)
+ (* Note that we can lookup the loan anywhere *)
let ek =
{
enter_shared_loans = true;
@@ -939,16 +944,18 @@ let rec end_borrow_in_env (config : C.config) (io : inner_outer)
assert (Option.is_none (lookup_borrow_opt ek l env));
env)
else
- (* Not the same abstraction: we need to end the whole abstraction *)
+ (* Not the same abstraction: we need to end the whole abstraction.
+ * By doing that we should have ended the target borrow (see the
+ * below sanity check) *)
let env = end_abstraction_in_env config abs_id env in
- (* Sanity check *)
+ (* Sanity check: we ended the target borrow *)
assert (Option.is_none (lookup_borrow_opt ek l env));
env
| Var _, _ ->
(* The loan is not inside the same abstraction (actually inside
* a non-abstraction value): we need to end the whole abstraction *)
let env = end_abstraction_in_env config abs_id env in
- (* Sanity check *)
+ (* Sanity check: we ended the target borrow *)
assert (Option.is_none (lookup_borrow_opt ek l env));
env))
| Ok (env, None) ->