diff options
author | Son Ho | 2022-01-13 21:56:36 +0100 |
---|---|---|
committer | Son Ho | 2022-01-13 21:56:36 +0100 |
commit | 0658739222a23474c5453eb32f282587ae8eb95e (patch) | |
tree | 0695538e1d6eab64ca16fcae97c0395d307082c1 /src/InterpreterUtils.ml | |
parent | 19783cea9664e5ac0b14419b4aa961716010aafb (diff) |
Update the projectors to ignore values when they don't contain regions
of interest
Diffstat (limited to 'src/InterpreterUtils.ml')
-rw-r--r-- | src/InterpreterUtils.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 65502126..92c92807 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -67,12 +67,18 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : in av -(** Create a loans projector from a symbolic value. *) -let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) : - V.typed_avalue = - let av = V.ASymbolic (V.AProjLoans svalue) in - let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in - av +(** Create a loans projector from a symbolic value. + + Checks if the projector will actually project some regions. If not, + returns [AIgnored] (`_`). + *) +let mk_aproj_loans_from_symbolic_value (regions : T.RegionId.Set.t) + (svalue : V.symbolic_value) : V.typed_avalue = + if ty_has_regions_in_set regions svalue.sv_ty then + let av = V.ASymbolic (V.AProjLoans svalue) in + let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in + av + else { V.value = V.AIgnored; ty = svalue.V.sv_ty } (** TODO: move *) let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool |