summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
authorSon Ho2021-12-07 11:56:13 +0100
committerSon Ho2021-12-07 11:56:13 +0100
commit612cf5370596bbd9733807c899dc53919b4029db (patch)
tree82c6badb2e0fb6ccee0ff87a8ea9e254fefebcbd /src/Interpreter.ml
parentf147bea1caf3acb6a7dd7b274aa50e4f91b42253 (diff)
Make update_loan_in_value work with visitors
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml41
1 files changed, 1 insertions, 40 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index fe1c1c6f..971bced8 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -176,8 +176,6 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) :
| None -> failwith "Unreachable"
| Some lc -> lc
-(*
-TODO: use this
(** Update a loan content in a value.
The loan is referred to by a borrow id.
@@ -209,44 +207,7 @@ let update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
*)
end
in
- (* We use exceptions *)
-obj#visit_typed_value () v*)
-
-(** Update a loan content in a value.
-
- The loan is referred to by a borrow id.
-
- This is a helper function: it might break invariants.
- *)
-let rec update_loan_in_value (ek : exploration_kind) (l : V.BorrowId.id)
- (nlc : V.loan_content) (v : V.typed_value) : V.typed_value =
- match v.V.value with
- | V.Concrete _ | V.Bottom | V.Symbolic _ -> v
- | V.Adt av ->
- let values = List.map (update_loan_in_value ek l nlc) av.field_values in
- let av = { av with field_values = values } in
- { v with value = Adt av }
- | V.Borrow bc -> (
- match bc with
- | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> v
- | V.MutBorrow (bid, mv) ->
- if ek.enter_mut_borrows then
- let v' =
- V.Borrow (V.MutBorrow (bid, update_loan_in_value ek l nlc mv))
- in
- { v with value = v' }
- else v)
- | V.Loan lc -> (
- match lc with
- | V.SharedLoan (bids, sv) ->
- if V.BorrowId.Set.mem l bids then { v with value = V.Loan nlc }
- else if ek.enter_shared_loans then
- let v' =
- V.Loan (V.SharedLoan (bids, update_loan_in_value ek l nlc sv))
- in
- { v with value = v' }
- else v
- | V.MutLoan bid -> if bid = l then { v with value = V.Loan nlc } else v)
+ obj#visit_typed_value () v
(** Update a loan content.