diff options
| author | Son Ho | 2022-01-14 11:56:28 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-14 11:56:28 +0100 |
| commit | 5b9e24c7ddcd53bc5c1a71a6efb6eecff757e151 (patch) | |
| tree | 55c66f8d64928a3bb7fd141b3e8cfacbe9708f44 /src/InterpreterProjectors.ml | |
| parent | e6ee5e6fda235e71283c6cccecbfc631457cc949 (diff) | |
Update aproj to make AEndedProjLoans take an `aproj option` and add the
AIgnoredProjBorrows variant
Diffstat (limited to 'src/InterpreterProjectors.ml')
| -rw-r--r-- | src/InterpreterProjectors.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index ad8c8f53..b1c61980 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -303,14 +303,16 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) -> (* Project over the field values *) let field_values = - List.map (mk_aproj_loans_from_symbolic_value regions) field_values + List.map + (mk_aproj_loans_value_from_symbolic_value regions) + field_values in (V.AAdt { V.variant_id; field_values }, original_sv_ty) | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_symbolic_value regions spc in + let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) if region_in_set r regions then @@ -323,7 +325,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_symbolic_value regions spc in + let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in (* Check if the region is in the set of projected regions (note that * we never project over static regions) *) if region_in_set r regions then |