diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 6 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index c4c090e3..029a2f1e 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -746,7 +746,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) a reference whose region has already ended). *) let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = - mk_fresh_symbolic_typed_value av.V.sv_ty + mk_fresh_symbolic_typed_value av.V.ty (** End a borrow identified by its borrow id in a context @@ -1136,11 +1136,11 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) | FoundAProjBorrows (sv, proj_ty) -> (* Replace the proj_borrows - there should be exactly one *) let ctx = - update_intersecting_aproj_borrows_non_shared regions sv + update_intersecting_aproj_borrows_non_shared abs.regions sv V.AEndedProjBorrows ctx in (* Give back a fresh symbolic value *) - let nsv = mk_fresh_symbolic_typed_value proj_ty in + let nsv = mk_fresh_symbolic_value proj_ty in let ctx = give_back_symbolic_value config sv nsv ctx in (* Reexplore *) end_abstraction_borrows config abs_id ctx diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 2886f642..b76ae28c 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -59,11 +59,11 @@ let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value = svalue (** Create a fresh symbolic value *) -let mk_fresh_symbolic_value (rty : T.rty) : V.symbolic_value = - let ty = Subst.erase_regions ty in +let mk_fresh_symbolic_typed_value (rty : T.rty) : V.typed_value = + let ty = Subst.erase_regions rty in (* Generate the fresh a symbolic value *) let value = mk_fresh_symbolic_value rty in - let value = V.Symbolic svalue in + let value = V.Symbolic value in { V.value; V.ty } (** Create a typed value from a symbolic value. *) |