summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index baf433c2..9a440648 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -703,8 +703,12 @@ let end_borrow_get_borrow_in_env (io : inner_outer)
match bc with
| V.AMutBorrow (bid, av) -> raise Unimplemented
| V.ASharedBorrow bid -> raise Unimplemented
- | V.AIgnoredMutBorrow av -> raise Unimplemented
- | V.AIgnoredSharedBorrow asb -> raise Unimplemented
+ | V.AIgnoredMutBorrow av ->
+ (* Nothing special to do *)
+ V.ABorrow (super#visit_AIgnoredMutBorrow outer av)
+ | V.AIgnoredSharedBorrow asb ->
+ (* Nothing special to do *)
+ V.ABorrow (super#visit_AIgnoredSharedBorrow outer asb)
method! visit_abs outer abs =
(* Update the outer abs *)