diff options
| author | Son Ho | 2022-04-20 16:09:14 +0200 |
|---|---|---|
| committer | Son Ho | 2022-04-20 16:09:14 +0200 |
| commit | b33e4bfc7a32efc6ebbd385328e6350e0e5802bc (patch) | |
| tree | d82cabccf4e999b23cd29ae1b5170d50fbc81d9e | |
| parent | 0d4e85006d06c51194db17a08055c00ee830124a (diff) | |
Add comments
| -rw-r--r-- | src/Values.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Values.ml b/src/Values.ml index d415df52..a3dfb84a 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -336,6 +336,9 @@ type aproj = (** The only purpose of [AEndedProjBorrows] is to store, for synthesis purposes, the symbolic value which was originally in the borrow projection, and the symbolic value which was generated and given back upon ending the borrow. + + The given back value is necessary for the synthesis. The orignal value is + useful to propagate naming constraints. *) | AIgnoredProjBorrows [@@deriving @@ -682,6 +685,10 @@ and aborrow_content = (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value that we gave back as a meta-value, to help with the synthesis, together with the initial consumed value (also as a meta-value). + + The given back value is necessary for the synthesis. The orignal consumed + value is useful to propagate naming constraints. + We also remember the child [avalue] because this structural information is useful for the synthesis (but not for the symbolic execution): in practice the child value should only contain ended borrows, ignored |