Merges branch 'master' into 'meilers_silicon_test_903'

.github/dependabot.yml

@@ -0,0 +1,12 @@
+version: 2
+
+updates:
+  - package-ecosystem: github-actions
+    directory: "/"
+    schedule:
+      interval: monthly
+      day: monday
+    groups:
+      all:
+        patterns:
+          - "*"

.github/workflows/carbon_silicon_ci.yml

@@ -30,7 +30,7 @@ jobs:
 
     steps:
     - name: Checkout backend
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: ${{ env.fork }}/${{ matrix.repo }}
         token: ${{ secrets.PAT }}
@@ -61,7 +61,7 @@ jobs:
         git push origin ci-test-${{ env.sha }}
 
     - name: Run CI
-      uses: convictional/trigger-workflow-and-wait@v1.6.0
+      uses: convictional/trigger-workflow-and-wait@v1.6.5
       with:
         owner: ${{ env.fork }}
         repo: ${{ matrix.repo }}

.github/workflows/scala.yml

@@ -27,9 +27,9 @@ jobs:
       shell: bash
       run: "git config --global core.autocrlf false"
     - name: Checkout
-      uses: actions/checkout@v2
+      uses: actions/checkout@v4
     - name: Set up Scala and JDK 1.${{ matrix.java }}
-      uses: olafurpg/setup-scala@v11
+      uses: olafurpg/setup-scala@v14
       with:
         # Should probably be changed to `temurin` once supported by `olafurpg/setup-scala`
         # See https://github.com/actions/setup-java#supported-distributions

.github/workflows/update_submodules.yml

@@ -18,7 +18,7 @@ jobs:
     steps:
     # Checkout the repository to the GitHub Actions runner
     - name: Checkout
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
       with:
         repository: viperproject/${{ matrix.repo }}
         token: ${{ secrets.PAT }}

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