Skip to content

Commit

Permalink
Update ReleaseNotes.md
Browse files Browse the repository at this point in the history
  • Loading branch information
tdardinier authored Jul 27, 2021
1 parent 4e36008 commit 3ea5422
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ReleaseNotes.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
### Changes in Viper Language

* **Breaking change**: Inhaling negative permission amounts now leads to a verification failure, whereas in the previous releases it was leading to an inconsistent state [(Silver, 522)](https://github.com/viperproject/silver/issues/522).
* **Future breaking change**: Currently, Viper checks the [injectivity of the receiver expression when exhaling quantified permissions](http://viper.ethz.ch/tutorial/?page=1&section=#receiver-expressions-and-injectivity), but not when inhaling quantified permissions. We [plan to change this](https://github.com/viperproject/silver/issues/531) in the January 2022 release, that Viper will also check the injectivity when inhaling quantified permissions. Since this is an important breaking change, this feature is only enabled in this release if the _--checkInjectivity_ flag is provided. This flag will be removed in the next release, and this injectivity check will be enabled by default.
* **Future breaking change**: Currently, Viper checks the [injectivity of the receiver expression when exhaling quantified permissions](http://viper.ethz.ch/tutorial/?page=1&section=#receiver-expressions-and-injectivity), but not when inhaling quantified permissions. We [plan to change this](https://github.com/viperproject/silver/issues/531) in the January 2022 release, that is Viper will also check the injectivity when inhaling quantified permissions. Since this is an important breaking change, this feature is only enabled in this release if the _--checkInjectivity_ flag is provided. This flag will be removed in the next release, and this injectivity check will be enabled by default.

### Backend-specific upgrades/changes

Expand Down

0 comments on commit 3ea5422

Please sign in to comment.