diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 4 | ||||
| -rw-r--r-- | src/SymbolicAstUtils.ml | 6 | ||||
| -rw-r--r-- | src/Values.ml | 8 |
4 files changed, 8 insertions, 12 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index ccd41747..bc5341c5 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -432,7 +432,7 @@ let give_back_symbolic_value (_config : C.config) | V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> () | V.FunCallRet | V.SynthInput -> failwith "Unrechable"); (* Store the given-back value as a meta-value for synthesis purposes *) - let mv = mk_typed_value_from_symbolic_value nsv in + let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) let subst (_abs : V.abs) local_given_back = (* Compute the projection over the given back value *) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 57e47df0..81f9d0d3 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -901,7 +901,7 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) *) let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value) - (subst : V.abs -> (V.typed_value * V.aproj) list -> V.aproj) + (subst : V.abs -> (V.msymbolic_value * V.aproj) list -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = (* Small helpers for sanity checks *) let updated = ref false in @@ -952,7 +952,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) to the couple (abstraction id, symbolic value). *) let lookup_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) - (ctx : C.eval_ctx) : (V.mvalue * V.aproj) list = + (ctx : C.eval_ctx) : (V.msymbolic_value * V.aproj) list = (* Small helpers for sanity checks *) let found = ref None in let set_found x = diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml index 264f9cad..5a329c8d 100644 --- a/src/SymbolicAstUtils.ml +++ b/src/SymbolicAstUtils.ml @@ -9,9 +9,9 @@ open InterpreterUtils type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's -type ended_loan = (V.mvalue, V.mvalue list) ended +type ended_loan = (V.typed_value, V.msymbolic_value list) ended -type ended_borrow = (V.mvalue, V.mvalue) ended +type ended_borrow = (V.typed_value, V.typed_value) ended type ended_loan_or_borrow = | EndedLoan of ended_loan @@ -45,7 +45,7 @@ let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list match aproj with | AEndedProjLoans (msv, []) -> (* The symbolic value was left unchanged *) - add_sloan [ mk_typed_value_from_symbolic_value msv ] + add_sloan [ msv ] | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl) | AEndedProjBorrows mv -> add_sborrow mv | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> diff --git a/src/Values.ml b/src/Values.ml index fe8daf30..6ab81f6b 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -252,7 +252,7 @@ class ['self] map_aproj_base = end type aproj = - | AProjLoans of symbolic_value * (mvalue * aproj) list + | AProjLoans of symbolic_value * (msymbolic_value * aproj) list (** A projector of loans over a symbolic value. Note that the borrows of a symbolic value may be spread between @@ -285,8 +285,6 @@ type aproj = We can later end the projector of loans if `s@0` is not referenced anywhere in the context below a projector of borrows which intersects this projector of loans. - - TODO: we should use an msymbolic_value, not an mvalue *) | AProjBorrows of symbolic_value * rty (** Note that an AProjBorrows only operates on a value which is not below @@ -296,14 +294,12 @@ type aproj = can't get updated/expanded: this means that we don't need to save any meta-value here. *) - | AEndedProjLoans of msymbolic_value * (mvalue * aproj) list + | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list (** An ended projector of loans over a symbolic value. See the explanations for [AProjLoans] Note that we keep the original symbolic value as a meta-value. - - TODO: we should use an msymbolic_value, not an mvalue *) | AEndedProjBorrows of mvalue (** The only purpose of [AEndedProjBorrows] is to store, for synthesis |