Prepare for KeY 2.12.4

.github/workflows/nightlydeploy.yml

@@ -3,7 +3,7 @@ name: Weekly Builds of KeY
 on:
   workflow_dispatch:
   schedule:
-    - cron:  '0 5 * * 1' # every monday morning
+    - cron: '0 5 * * 1' # every monday morning
 
 permissions:
   contents: write
@@ -12,7 +12,6 @@ permissions:
 env:
   JAVA_VERSION: 21
 
-
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -24,84 +23,51 @@ jobs:
           java-version: ${{ env.JAVA_VERSION }}
           distribution: 'temurin'
           cache: 'gradle'
+          gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }}
+          gpg-passphrase: ${{ secrets.GPG_PASSPHRASE }}
 
       - name: Setup Gradle
         uses: gradle/actions/setup-gradle@v5
 
       - name: Build with Gradle
-        run: ./gradlew --parallel assemble
+        run: ./gradlew --parallel assemble javadoc alldoc
 
-  doc:
-    needs: [build]
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v6
-      - name: Set up JDK ${{ env.JAVA_VERSION }}
-        uses: actions/setup-java@v5
+      - name: Upload ShadowJar
+        uses: actions/upload-artifact@v7
         with:
-          java-version: ${{ env.JAVA_VERSION }}
-          distribution: 'temurin'
-          cache: 'gradle'
-
-      - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v5
-
-      - name: Build Documentation with Gradle
-        run: ./gradlew alldoc
+          name: shadowjars
+          path: "*/build/libs/*-exe.jar"
+          retention-days: 1
 
       - name: Package
         run: tar cvf key-javadoc.tar.xz build/docs/javadoc
 
-  deploy:
-    needs: [build, doc]
-    runs-on: ubuntu-latest
-    steps:
       - name: Upload Javadoc
         uses: actions/upload-artifact@v7
         with:
           name: javadoc
-          path: "javadoc.tar.xz"
-
-      - name: Upload ShadowJar
-        uses: actions/upload-artifact@v7
-        with:
-          name: shadowjars
-          path: "*/build/libs/*-exe.jar"
+          path: "key-javadoc.tar.xz"
+          retention-days: 1
 
       - name: Delete previous nightly release
         continue-on-error: true
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          gh release delete nightly --yes --cleanup-tag 
+          gh release delete KEY-2.12.4-Release-Candidate --yes --cleanup-tag 
 
       - name: Create nightly release
         id: create_release
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        run: |          
-          gh release create --generate-notes --title "Nightly Release" \
+        run: |
+          gh release create --generate-notes --title "KeY 2.12.4 Pre-Release" \
              --prerelease --notes-start-tag KEY-2.12.3 \
-             nightly key.ui/build/libs/key-*-exe.jar
-
-  deploy-maven:
-    needs: [ build, doc ]
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v6
-      - name: Set up JDK ${{ env.JAVA_VERSION }}
-        uses: actions/setup-java@v5
-        with:
-          java-version: ${{ env.JAVA_VERSION }}
-          distribution: 'temurin'
-          cache: 'gradle'
-
-      - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v5
+             KEY-2.12.4-Release-Candidate key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz
 
+      - run: export GPG_TTY=$(tty)
       - name: Upload to SNAPSHOT repository
-        run: ./gradlew publishMavenJavaPublicationToKEYLABRepository
+        run: ./gradlew --parallel publishMavenJavaPublicationToKEYLABRepository
         env:
           BUILD_NUMBER: "SNAPSHOT"
           GITLAB_DEPLOY_TOKEN: ${{ secrets.GITLAB_DEPLOY_TOKEN }}
-

LICENSE.TXT

@@ -3,7 +3,7 @@
        Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
                                Universitaet Koblenz-Landau, Germany
                                Chalmers University of Technology, Sweden
-       Copyright (C) 2011-2019 Karlsruhe Institute of Technology, Germany
+       Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany
                                Technical University Darmstadt, Germany
                                Chalmers University of Technology, Sweden
 

README.md

@@ -14,7 +14,7 @@ For more information, refer to
   * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4),
   * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/)
 
-The current version of KeY is 2.12.2, licensed under GPL v2.
+The current version of KeY is 2.12.4, licensed under GPL v2.
 
 
 Feel free to use the project templates to get started using KeY:

key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java

@@ -33,7 +33,6 @@
  */
 public class SwitchToIf extends ProgramTransformer {
 
-    private boolean noNewBreak = true;
 
     /**
      * creates a switch-to-if ProgramTransformer
@@ -49,6 +48,7 @@ public ProgramElement[] transform(ProgramElement pe, Services services,
             SVInstantiations insts) {
         Switch sw = (Switch) pe;
 
+
         VariableNamer varNamer = services.getVariableNamer();
 
         Label l = varNamer.getTemporaryNameProposal("_l");
@@ -62,7 +62,8 @@ public ProgramElement[] transform(ProgramElement pe, Services services,
         Statement s =
             KeYJavaASTFactory.declare(name, sw.getExpression().getKeYJavaType(services, ec));
 
-        sw = changeBreaks(sw, newBreak);
+        final var changeBreakResult = changeBreaks(sw, newBreak, true);
+        sw = (Switch) changeBreakResult.result;
         Statement currentBlock = null;
         for (int i = sw.getBranchCount() - 1; 0 <= i; i--) {
             if (sw.getBranchAt(i) instanceof Default) {
@@ -96,7 +97,7 @@ public ProgramElement[] transform(ProgramElement pe, Services services,
             // empty switch of primitive type, the expression can still have side-effects
             result = KeYJavaASTFactory.block(s, KeYJavaASTFactory.assign(exV, sw.getExpression()));
         }
-        if (noNewBreak) {
+        if (changeBreakResult.noNewBreak) {
             return new ProgramElement[] { result };
         } else {
             return new ProgramElement[] {
@@ -130,69 +131,103 @@ private If mkIfNullCheck(Services services, ProgramVariable var, Statement elseB
     /**
      * Replaces all breaks in <code>sw</code>, whose target is sw, with <code>b</code>
      */
-    private Switch changeBreaks(Switch sw, Break b) {
+    private ChangeBreakResult changeBreaks(Switch sw, Break b, boolean noNewBreak) {
         int n = sw.getBranchCount();
         Branch[] branches = new Branch[n];
         for (int i = 0; i < n; i++) {
-            branches[i] = (Branch) recChangeBreaks(sw.getBranchAt(i), b);
+            final var branch = recChangeBreaks(sw.getBranchAt(i), b, noNewBreak);
+            noNewBreak = branch.noNewBreak;
+            branches[i] = (Branch) branch.result;
         }
-        return KeYJavaASTFactory.switchBlock(sw.getExpression(), branches);
+        return new ChangeBreakResult(KeYJavaASTFactory.switchBlock(sw.getExpression(), branches),
+            noNewBreak);
     }
 
-    private ProgramElement recChangeBreaks(ProgramElement p, Break b) {
+    private ChangeBreakResult recChangeBreaks(ProgramElement p, Break b, boolean noNewBreak) {
         if (p == null) {
             return null;
         }
         if (p instanceof Break && ((Break) p).getLabel() == null) {
-            noNewBreak = false;
-            return b;
+            return new ChangeBreakResult(b, false);
         }
         if (p instanceof Branch) {
             Statement[] s = new Statement[((Branch) p).getStatementCount()];
             for (int i = 0; i < ((Branch) p).getStatementCount(); i++) {
-                s[i] = (Statement) recChangeBreaks(((Branch) p).getStatementAt(i), b);
+                final ChangeBreakResult r =
+                    recChangeBreaks(((Branch) p).getStatementAt(i), b, noNewBreak);
+                noNewBreak = r.noNewBreak;
+                s[i] = (Statement) r.result;
             }
             if (p instanceof Case) {
-                return KeYJavaASTFactory.caseBlock(((Case) p).getExpression(), s);
+                return new ChangeBreakResult(
+                    KeYJavaASTFactory.caseBlock(((Case) p).getExpression(), s),
+                    noNewBreak);
             }
             if (p instanceof Default) {
-                return KeYJavaASTFactory.defaultBlock(s);
+                return new ChangeBreakResult(
+                    KeYJavaASTFactory.defaultBlock(s),
+                    noNewBreak);
             }
             if (p instanceof Catch) {
-                return KeYJavaASTFactory.catchClause(((Catch) p).getParameterDeclaration(), s);
+                return new ChangeBreakResult(
+                    KeYJavaASTFactory.catchClause(((Catch) p).getParameterDeclaration(), s),
+                    noNewBreak);
             }
             if (p instanceof Finally) {
-                return KeYJavaASTFactory.finallyBlock(s);
+                return new ChangeBreakResult(KeYJavaASTFactory.finallyBlock(s),
+                    noNewBreak);
             }
             if (p instanceof Then) {
-                return KeYJavaASTFactory.thenBlock(s);
+                return new ChangeBreakResult(
+                    KeYJavaASTFactory.thenBlock(s),
+                    noNewBreak);
             }
             if (p instanceof Else) {
-                return KeYJavaASTFactory.elseBlock(s);
+                return new ChangeBreakResult(
+                    KeYJavaASTFactory.elseBlock(s),
+                    noNewBreak);
             }
         }
         if (p instanceof If) {
-            return KeYJavaASTFactory.ifElse(((If) p).getExpression(),
-                (Then) recChangeBreaks(((If) p).getThen(), b),
-                (Else) recChangeBreaks(((If) p).getElse(), b));
+            final ChangeBreakResult then = recChangeBreaks(((If) p).getThen(), b, noNewBreak);
+            noNewBreak = then.noNewBreak;
+            final ChangeBreakResult _else = recChangeBreaks(((If) p).getElse(), b, noNewBreak);
+            noNewBreak = _else.noNewBreak;
+            return new ChangeBreakResult(
+                KeYJavaASTFactory.ifElse(((If) p).getExpression(),
+                    (Then) then.result, (Else) _else.result),
+                noNewBreak);
+
         }
         if (p instanceof StatementBlock) {
             Statement[] s = new Statement[((StatementBlock) p).getStatementCount()];
             for (int i = 0; i < ((StatementBlock) p).getStatementCount(); i++) {
-                s[i] = (Statement) recChangeBreaks(((StatementBlock) p).getStatementAt(i), b);
+                final ChangeBreakResult blockStmnt =
+                    recChangeBreaks(((StatementBlock) p).getStatementAt(i), b, noNewBreak);
+                noNewBreak = blockStmnt.noNewBreak;
+                s[i] = (Statement) blockStmnt.result;
             }
-            return KeYJavaASTFactory.block(s);
+            return new ChangeBreakResult(
+                KeYJavaASTFactory.block(s),
+                noNewBreak);
         }
         if (p instanceof Try) {
             int n = ((Try) p).getBranchCount();
             Branch[] branches = new Branch[n];
             for (int i = 0; i < n; i++) {
-                branches[i] = (Branch) recChangeBreaks(((Try) p).getBranchAt(i), b);
+                final ChangeBreakResult branch =
+                    recChangeBreaks(((Try) p).getBranchAt(i), b, noNewBreak);
+                noNewBreak = branch.noNewBreak;
+                branches[i] = (Branch) branch.result;
             }
-            return KeYJavaASTFactory
-                    .tryBlock((StatementBlock) recChangeBreaks(((Try) p).getBody(), b), branches);
+            final var block = recChangeBreaks(((Try) p).getBody(), b, noNewBreak);
+            noNewBreak = block.noNewBreak;
+            return new ChangeBreakResult(
+                KeYJavaASTFactory
+                        .tryBlock((StatementBlock) block.result, branches),
+                noNewBreak);
         }
-        return p;
+        return new ChangeBreakResult(p, noNewBreak);
     }
 
     /**
@@ -216,4 +251,7 @@ private StatementBlock collectStatements(Switch s, int count) {
         return KeYJavaASTFactory.block(stats);
     }
 
+    record ChangeBreakResult(ProgramElement result, boolean noNewBreak) {
+    }
+
 }

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java

@@ -186,6 +186,8 @@ public Taclet generateRelationalRepresentsTaclet(Name tacletName, JTerm original
         tacletBuilder.setFind(findTerm);
         tacletBuilder.addTacletGoalTemplate(axiomTemplate);
         tacletBuilder.addVarsNotFreeIn(schemaAxiom.boundVars, selfSV);
+        tacletBuilder.setApplicationRestriction(
+            new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL));
         for (SchemaVariable heapSV : heapSVs) {
             tacletBuilder.addVarsNotFreeIn(schemaAxiom.boundVars, heapSV);
         }

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java

@@ -4,12 +4,6 @@ public final class String extends java.lang.Object implements java.io.Serializab
 {
    // public final static java.util.Comparator CASE_INSENSITIVE_ORDER;
 
-   /*@ normal_behavior
-       ensures \result == \dl_seqLen(\dl_strContent(this));
-    */
-   public /*@pure*/ int length();
-
-
    /*@
    public normal_behavior
       requires true;