From 8a3d17974b3359bead6fec26805acf10a66b8e6e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 19 Mar 2026 15:57:39 +0100 Subject: [PATCH 1/6] Prepare for KeY 2.12.4 --- .github/workflows/nightlydeploy.yml | 2 +- LICENSE.TXT | 2 +- README.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index c655799b929..707c970c50e 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -81,7 +81,7 @@ jobs: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | gh release create --generate-notes --title "Nightly Release" \ - --prerelease --notes-start-tag KEY-2.12.3 \ + --prerelease --notes-start-tag KEY-2.12.4-rc \ nightly key.ui/build/libs/key-*-exe.jar deploy-maven: diff --git a/LICENSE.TXT b/LICENSE.TXT index dbafedb51f2..1a701bdf921 100644 --- a/LICENSE.TXT +++ b/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 diff --git a/README.md b/README.md index e9d834c472a..9909a37f752 100644 --- a/README.md +++ b/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: From b2e1da53640708a9d0823cc5b98f6f3859d00d25 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 20 Mar 2026 13:58:50 +0100 Subject: [PATCH 2/6] Fix tag --- .github/workflows/nightlydeploy.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 707c970c50e..c655799b929 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -81,7 +81,7 @@ jobs: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | gh release create --generate-notes --title "Nightly Release" \ - --prerelease --notes-start-tag KEY-2.12.4-rc \ + --prerelease --notes-start-tag KEY-2.12.3 \ nightly key.ui/build/libs/key-*-exe.jar deploy-maven: From c1fd38f332c47f8730c3caff7afd249a944df026 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 11 Mar 2026 18:17:21 +0100 Subject: [PATCH 3/6] Add missing inSameUpdateLevel to represents-taclets --- .../de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index c313592f4de..8d115bb3673 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/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); } From 1693170e257ea01e8677c520e380523f571aba71 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 11 Mar 2026 13:03:15 +0100 Subject: [PATCH 4/6] Make switchToIf stateless --- .../key/rule/metaconstruct/SwitchToIf.java | 88 +++++++++++++------ 1 file changed, 63 insertions(+), 25 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java index 297b663ad3c..624237c6f03 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java +++ b/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 sw, whose target is sw, with b */ - 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) { + } + } From e04091b71dbb3457ed8636961f9ab66542aafc95 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 10 Mar 2026 18:19:05 +0100 Subject: [PATCH 5/6] Fix double declaration of method String#length in javaRedux: String.java --- .../de/uka/ilkd/key/java/JavaRedux/java/lang/String.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java index 9e3a2489693..7ff333e05b0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java +++ b/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; From 0198756d454f4748567b9f5a393c8af7937bc679 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 24 Mar 2026 13:39:02 +0100 Subject: [PATCH 6/6] use updated nightdeploy script from JP 3.0.0 pre release branch --- .github/workflows/nightlydeploy.yml | 68 ++++++++--------------------- 1 file changed, 17 insertions(+), 51 deletions(-) diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index c655799b929..7065c0b77e3 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.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 }} -