views: yet another bugfix (#15447)

* views: yet another bugfix

* views: extended the spec

* views: take into account potential hidden mutations via proc calls
This commit is contained in:
Andreas Rumpf 2020-10-01 15:04:36 +02:00 • committed by GitHub
commit ab405c936e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
5 changed files with 44 additions and 10 deletions

View file

@ -1988,6 +1988,22 @@ borrow operation of ``v`` even though a human being can easily see that it
will never do that at runtime.
Start of a borrow
-----------------
A borrow starts with one of the following:
- The assignment of a non-view-type to a view-type.
- The assingment of a location that is derived from a local parameter
to a view-type.
End of a borrow
---------------
A borrow operation ends with the last usage of the view variable.
Reborrows
---------