summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
authorSon Ho2022-04-21 11:12:34 +0200
committerSon Ho2022-04-21 11:12:34 +0200
commit66862a29cf023ca4d586479a9690dc4f61d8573c (patch)
tree59103212e80b7561ffded9d612dde5ac01f043d3 /src/InterpreterBorrows.ml
parentb33e4bfc7a32efc6ebbd385328e6350e0e5802bc (diff)
Work on pretty names
Diffstat (limited to '')
-rw-r--r--src/InterpreterBorrows.ml8
1 files changed, 3 insertions, 5 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 065a39b9..89dfb274 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1202,12 +1202,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
^ aborrow_content_to_string ctx bc));
let ctx =
match bc with
- | V.AMutBorrow (mv, bid, av) ->
+ | V.AMutBorrow (_mv, bid, av) ->
(* First, convert the avalue to a (fresh symbolic) value *)
let sv = convert_avalue_to_given_back_value abs.kind av in
(* Replace the mut borrow to register the fact that we ended
* it and store with it the freshly generated given back value *)
- let ended_borrow = V.ABorrow (V.AEndedMutBorrow (mv, sv, av)) in
+ let ended_borrow = V.ABorrow (V.AEndedMutBorrow (sv, av)) in
let ctx = update_aborrow ek_all bid ended_borrow ctx in
(* Give the value back *)
let sv = mk_typed_value_from_symbolic_value sv in
@@ -1256,9 +1256,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
(* Generate a fresh symbolic value *)
let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
(* Replace the proj_borrows - there should be exactly one *)
- let ended_borrow =
- V.AEndedProjBorrows { original = sv; given_back = nsv }
- in
+ let ended_borrow = V.AEndedProjBorrows nsv in
let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
(* Give back the symbolic value *)
let ctx =