summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-27 00:32:31 +0100
committerSon Ho2022-01-27 00:32:31 +0100
commit4e140fb31464173c7692668419f5938e34177015 (patch)
tree8f151907821f7f8e9f84695cdd04ec0c8a9f248e /src
parent1e3e6f6ecdbc277322f3631dac683fe938134d0c (diff)
Make give_back_symbolic_value fail in case we need to reinsert inside an
AProjLoans: there is something wrong
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml16
1 files changed, 14 insertions, 2 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 24521335..ad7b5b2c 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -437,6 +437,8 @@ let give_back_symbolic_value (_config : C.config)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
let subst (_abs : V.abs) local_given_back =
+ (* See the below comments: there is something wrong here *)
+ let _ = raise Errors.Unimplemented in
(* Compute the projection over the given back value *)
let child_proj =
match nsv.sv_kind with
@@ -450,11 +452,21 @@ let give_back_symbolic_value (_config : C.config)
* (and MUST) forget the borrows *)
V.AIgnoredProjBorrows
| V.FunCallGivenBack ->
- (* The value was fed as input to a function, and was given back *)
+ (* TODO: there is something wrong here.
+ * Consider this:
+ * ```
+ * abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+ * abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+ * ```
+ *
+ * Upon ending abs1, we give back some fresh symbolic value `s1`,
+ * that we reinsert where the loan for `s0` is. However, the mutable
+ * borrow in the type `&'a mut T` was ended: we give back a value of
+ * type `T`! We thus *mustn't* introduce a projector here.
+ *)
V.AProjBorrows (nsv, sv.V.sv_ty)
| _ -> failwith "Unreachable"
in
- (* TODO: this actually doesn't work, or at least there is something subtle... *)
V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx