diff options
Diffstat (limited to 'src/Values.ml')
| -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 |