summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/InterpreterBorrows.ml')
-rw-r--r--src/InterpreterBorrows.ml13
1 files changed, 13 insertions, 0 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 20314120..487e308a 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1063,6 +1063,15 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
| V.AIgnoredSharedLoan _ ->
super#visit_aloan_content env lc
+ method! visit_loan_content env lc =
+ match lc with
+ | V.MutLoan _ ->
+ (* The mut loan linked to the mutable borrow present in a shared
+ * value in an abstraction should be in an AProjBorrows *)
+ failwith "Unreachable"
+ | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
+ (** We may need to visit loan contents because of shared values *)
+
method! visit_aproj env sproj =
(match sproj with
| V.AProjBorrows (_, _)
@@ -1149,6 +1158,10 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
| V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
());
super#visit_aproj env sproj
+
+ method! visit_borrow_content env bc =
+ (* TODO: this happens because of shared values *)
+ raise Errors.Unimplemented
end
in
(* Lookup the abstraction *)