summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/InterpreterBorrows.ml')
-rw-r--r--src/InterpreterBorrows.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index d17991ea..19e5716f 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -439,6 +439,8 @@ let give_back_symbolic_value (_config : C.config) (sv : V.symbolic_value)
in
V.AEndedProjLoans child_proj
in
+ (* TODO: we need to use the regions!! *)
+ raise Errors.Unimplemented;
substitute_aproj_loans_with_id sv subst ctx
(** Auxiliary function to end borrows. See [give_back].