summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-25 23:13:33 +0100
committerSon Ho2022-01-25 23:13:33 +0100
commit345f85f101974ce9347b4eed083a96cdf125085e (patch)
treed9be1e6f717e99fbfe375b6706c1ad79d6fe6597 /src
parent592a2113734078290d4406df7804bfc128865958 (diff)
Replace another occurrence of mvalue with msymbolic_value
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml4
-rw-r--r--src/SymbolicAstUtils.ml2
-rw-r--r--src/Values.ml2
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.