diff options
author | Son Ho | 2022-01-13 21:24:58 +0100 |
---|---|---|
committer | Son Ho | 2022-01-13 21:24:58 +0100 |
commit | e9c3dfc34d7cac0d2449b4d11db5adf7218b25db (patch) | |
tree | ac838adf50a7051918a9d2169f139b03bde14173 /src/InterpreterExpansion.ml | |
parent | 01cde7e6ddc047c2ea13365a67555ed1defbe1e4 (diff) |
Introduce ended borrow/loan projectors over symbolic values
Diffstat (limited to 'src/InterpreterExpansion.ml')
-rw-r--r-- | src/InterpreterExpansion.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index e19f8bb4..18ec1ecc 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -75,6 +75,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) let proj_regions = current_abs.regions in let ancestors_regions = current_abs.ancestors_regions in match (aproj, proj_kind) with + | (V.AEndedProjLoans | V.AEndedProjBorrows), _ -> V.ASymbolic aproj | V.AProjLoans sv, LoanProj -> (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then @@ -311,6 +312,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) match reborrow_ashared (Option.get proj_regions) sv proj_ty with | None -> super#visit_ASymbolic proj_regions aproj | Some asb -> V.ABorrow (V.AProjSharedBorrow asb)) + | AEndedProjLoans | AEndedProjBorrows -> V.ASymbolic aproj end in (* Call the visitor *) |