diff options
author | Son Ho | 2022-04-21 11:12:34 +0200 |
---|---|---|
committer | Son Ho | 2022-04-21 11:12:34 +0200 |
commit | 66862a29cf023ca4d586479a9690dc4f61d8573c (patch) | |
tree | 59103212e80b7561ffded9d612dde5ac01f043d3 /src/InterpreterBorrows.ml | |
parent | b33e4bfc7a32efc6ebbd385328e6350e0e5802bc (diff) |
Work on pretty names
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterBorrows.ml | 8 |
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 = |