diff options
Diffstat (limited to 'src/InterpreterExpansion.ml')
| -rw-r--r-- | src/InterpreterExpansion.ml | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index aebcda3c..e19f8bb4 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -63,15 +63,17 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) object inherit [_] C.map_eval_ctx as super - method! visit_abs proj_regions abs = - assert (Option.is_none proj_regions); - let proj_regions = Some abs.V.regions in - super#visit_abs proj_regions abs + method! visit_abs current_abs abs = + assert (Option.is_none current_abs); + let current_abs = Some abs in + super#visit_abs current_abs abs (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) - method! visit_ASymbolic proj_regions aproj = - let proj_regions = Option.get proj_regions in + method! visit_ASymbolic current_abs aproj = + let current_abs = Option.get current_abs in + let proj_regions = current_abs.regions in + let ancestors_regions = current_abs.ancestors_regions in match (aproj, proj_kind) with | V.AProjLoans sv, LoanProj -> (* Check if this is the symbolic value we are looking for *) @@ -85,7 +87,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) projected_value.V.value else (* Not the searched symbolic value: nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj + super#visit_ASymbolic (Some current_abs) aproj | V.AProjBorrows (sv, proj_ty), BorrowProj -> (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then @@ -101,16 +103,16 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) (* Apply the projector *) let projected_value = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - proj_regions expansion proj_ty + proj_regions ancestors_regions expansion proj_ty in (* Replace *) projected_value.V.value else (* Not the searched symbolic value: nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj + super#visit_ASymbolic (Some current_abs) aproj | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> (* Nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj + super#visit_ASymbolic (Some current_abs) aproj end in (* Apply the expansion *) |