From 345f85f101974ce9347b4eed083a96cdf125085e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jan 2022 23:13:33 +0100 Subject: Replace another occurrence of mvalue with msymbolic_value --- src/InterpreterBorrows.ml | 4 +--- src/SymbolicAstUtils.ml | 2 +- src/Values.ml | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index bc5341c5..6cf2c88f 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1208,9 +1208,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 (mk_typed_value_from_symbolic_value 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 = diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml index 5a329c8d..6e9f10b0 100644 --- a/src/SymbolicAstUtils.ml +++ b/src/SymbolicAstUtils.ml @@ -11,7 +11,7 @@ type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's type ended_loan = (V.typed_value, V.msymbolic_value list) ended -type ended_borrow = (V.typed_value, V.typed_value) ended +type ended_borrow = (V.typed_value, V.msymbolic_value) ended type ended_loan_or_borrow = | EndedLoan of ended_loan diff --git a/src/Values.ml b/src/Values.ml index 6ab81f6b..45bd5b6e 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -301,7 +301,7 @@ type aproj = Note that we keep the original symbolic value as a meta-value. *) - | AEndedProjBorrows of mvalue + | AEndedProjBorrows of msymbolic_value (** The only purpose of [AEndedProjBorrows] is to store, for synthesis purposes, the symbolic value which was generated and given back upon ending the borrow. -- cgit v1.2.3