diff options
author | Son Ho | 2022-01-19 01:24:35 +0100 |
---|---|---|
committer | Son Ho | 2022-01-19 01:24:35 +0100 |
commit | 2c93d514d6d62f8eccba47b1efefa2db1e56954e (patch) | |
tree | a3addf7bad4824f9a6ad7d5acaee59c61b405f21 /src/Values.ml | |
parent | c0f230dc6c331e9eb120900e8c31a03e1f5ab476 (diff) |
Implement the sanity checks for consumption of symbolic values by
abstractions (as input or given back values)
Diffstat (limited to '')
-rw-r--r-- | src/Values.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Values.ml b/src/Values.ml index a64d4467..6386f8db 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -232,6 +232,10 @@ type aproj = (** When ending a proj_loans over a symbolic value, we may need to insert (and keep track of) a proj_borrows over the given back value, if the symbolic value was consumed by an abstraction then updated. + + Rk.: for now this is useless, because we forbid borrow overwrites on + returned values. A consequence is that when a proj_loans over a symbolic + value ends, we don't project the given back value. *) | AEndedProjBorrows (* TODO: remove AEndedProjBorrows? We might need it for synthesis, to contain |