diff options
author | Son Ho | 2022-01-06 18:20:24 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 18:20:24 +0100 |
commit | f3982cbe9782405b50b04c948ba7cb0bd89ef85f (patch) | |
tree | 2df26310f1e67980a8b6f6ff278bd71bf0791eb4 /src/InterpreterBorrows.ml | |
parent | 7137e0733650e0ce37eff4ff805c95543f2c1161 (diff) |
Make the symbolic, borrow, region and abstration counters global and
stateful
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterBorrows.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 3cfa78e0..a18ccefb 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -619,15 +619,14 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) be expanded (because expanding this symbolic value would require expanding a reference whose region has already ended). *) -let convert_avalue_to_value (av : V.typed_avalue) (ctx : C.eval_ctx) : - C.eval_ctx * V.typed_value = +let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = (* Convert the type *) let ty = Subst.erase_regions av.V.ty in (* Generate the fresh a symbolic value *) - let ctx, sv_id = C.fresh_symbolic_value_id ctx in + let sv_id = C.fresh_symbolic_value_id () in let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in let value = V.Symbolic svalue in - (ctx, { V.value; V.ty }) + { V.value; V.ty } (** End a borrow identified by its borrow id in a context @@ -901,7 +900,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) match bc with | V.AMutBorrow (bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) - let ctx, v = convert_avalue_to_value av ctx in + let v = convert_avalue_to_value av in give_back_value config bid v ctx | V.ASharedBorrow bid -> give_back_shared config bid ctx | V.AProjSharedBorrow _ -> |