Update ReleaseNotes.md

Author: marcoeilers

Diff for: ReleaseNotes.md

@@ -4,7 +4,7 @@
 
 ### Changes in Viper Language
 
-- The semantics of permission amounts in functions has changed. When checking function preconditions, concrete permission amounts are ignored; instead, we only distinguish between zero and any positive amounts. Thus, the following assertions all have the same meaning in a function precondition: ``acc(x.f, write)`` or ``acc(x.f, wildcard)`` or ``acc(x.f, 1/2)`` or ``acc(x.f, b ? write : 1/2)`` or  ``acc(x.f) && acc(x.f)`` or ``acc(x.f, 2/1)`` all just require checking that a caller has some positive permission amount to ``x.f``. The same is true for predicate permissions. As a result, inside a function, one can no longer assume non-aliasing based on permission amounts. Additionally, when verifying well-definedness of a function, again all permission amounts are ignored (with the exception of distinguishing between zero and something positive as stated before), so one can for example unfold a whole predicate inside a function whose precondition only asks for half that predicate. Programs may still use concrete permission amounts in functions to preserve backward-compatibility, but such amounts will be meaningless and will result in a warning. https://github.com/viperproject/silicon/pull/877
+- The semantics of permission amounts in functions has changed. When checking function preconditions, concrete permission amounts are ignored; instead, we only distinguish between zero and any positive amounts. Thus, the following assertions all have the same meaning in a function precondition: ``acc(x.f, write)`` or ``acc(x.f, wildcard)`` or ``acc(x.f, 1/2)`` or ``acc(x.f, b ? write : 1/2)`` or  ``acc(x.f) && acc(x.f)`` or ``acc(x.f, 2/1)`` all just require checking that a caller has some positive permission amount to ``x.f``. The same is true for predicate permissions. As a result, inside a function, one can no longer assume non-aliasing based on permission amounts. Additionally, when verifying well-definedness of a function, again all permission amounts are ignored (with the exception of distinguishing between zero and something positive as stated before), so one can for example unfold a whole predicate inside a function whose precondition only asks for half that predicate. Programs may still use concrete permission amounts in functions to preserve backward-compatibility, but such amounts will be meaningless and will result in a warning. The old permission semantics is still available and can be enabled using the new command line flag ``--respectFunctionPrePermAmounts``. https://github.com/viperproject/silicon/pull/877
 - Added a new expression ``asserting (a) in e``, which checks that ``a`` holds and subsequently evaluates to ``e``. https://github.com/viperproject/silver/pull/814
 
 ### API Changes