Merge branch 'main' into weigl/codequality

.github/workflows/code_quality.yml

@@ -19,10 +19,10 @@ jobs:
           java-version: 21
           distribution: 'corretto'
           cache: 'gradle'
+      - name: Setup Gradle
+        uses: gradle/actions/[email protected]
       - name: Build with Gradle
-        uses: gradle/[email protected]
-        with:
-          arguments: -DENABLE_NULLNESS=true compileTest
+        run: ./gradlew -DENABLE_NULLNESS=true compileTest
 
   formatting:
     runs-on: ubuntu-latest
@@ -36,4 +36,4 @@ jobs:
       - name: Build with Gradle
         uses: gradle/[email protected]
         with:
-          arguments: --continue spotlessCheck
+          arguments: --continue spotlessCheck

.github/workflows/gradle-publish.yml

@@ -21,17 +21,15 @@ jobs:
         cache: 'gradle'
         server-id: github # Value of the distributionManagement/repository/id field of the pom.xml
 
+    - name: Setup Gradle
+      uses: gradle/actions/[email protected]
     - name: Assemble with Gradle
-      uses: gradle/[email protected]
-      with:
-        arguments: assemble
+      run: ./gradlew assemble
 
     # The USERNAME and TOKEN need to correspond to the credentials environment variables used in
     # the publishing section of your build.gradle
     - name: Publish to GitHub Packages
-      uses: gradle/[email protected]
-      with:
-        arguments: publish
+      run: ./gradlew publish
       env:
         USERNAME: ${{ github.actor }}
         TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/javadoc.yml

@@ -18,11 +18,10 @@ jobs:
           java-version: '21'
           distribution: 'corretto'
           cache: 'gradle'
-
-      - name: Build with Gradle
-        uses: gradle/[email protected]
-        with:
-          arguments: alldoc
+      - name: Setup Gradle
+        uses: gradle/actions/[email protected]
+      - name: Build Documentation with Gradle
+        run: ./gradlew alldoc
 
       - name: Package
         run: tar cvfj javadoc.tar.bz2 build/docs/javadoc

.github/workflows/nightlydeploy.yml

@@ -30,10 +30,10 @@ jobs:
           java-version: 17
           distribution: 'temurin'
 
+      - name: Setup Gradle
+        uses: gradle/actions/[email protected]
       - name: Build with Gradle
-        uses: gradle/[email protected]
-        with:
-          arguments: --parallel assemble
+        run: ./gradlew --parallel assemble
 
       - name: Delete previous nightly release
         continue-on-error: true

.github/workflows/opttest.yml

@@ -24,10 +24,10 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue ${{ matrix.tests }}
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Test with Gradle
+        run: ./gradlew --continue ${{ matrix.tests }}
 
       - name: Upload test results
         uses: actions/upload-artifact@v4

.github/workflows/tests.yml

@@ -37,10 +37,10 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Test with Gradle
+        run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
       - name: Upload test results
         uses: actions/upload-artifact@v4
@@ -86,11 +86,10 @@ jobs:
         run: .github/dlsmt.sh
         shell: bash
 
-
+      - name: Setup Gradle
+        uses: gradle/actions/[email protected]
       - name: "Running tests: ${{ matrix.test }}"
-        uses: gradle/[email protected]
-        with:
-          arguments: --continue ${{ matrix.test }}
+        run: ./gradlew --continue ${{ matrix.test }}
 
       - name: Upload test results
         uses: actions/upload-artifact@v4

.github/workflows/tests_winmac.yml

@@ -28,10 +28,11 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/[email protected]
-        with:
-          arguments: --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
+      - name: Setup Gradle
+        uses:
+          gradle/actions/[email protected]
+      - name: Test with Gradle
+        run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
       - name: Upload test results
         uses: actions/upload-artifact@v4
@@ -74,10 +75,10 @@ jobs:
       - name: Install SMT-Solvers
         run: .github/dlsmt.sh
 
+      - name: Setup Gradle
+        uses: gradle/actions/[email protected]
       - name: "Running tests: ${{ matrix.test }}"
-        uses: gradle/[email protected]
-        with:
-          arguments: --continue ${{ matrix.test }}
+        run: ./gradlew --continue ${{ matrix.test }}
 
       - name: Upload test results
         uses: actions/upload-artifact@v4

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -681,6 +681,18 @@ public ChoiceExpr visitOption_expr_paren(KeYParser.Option_expr_parenContext ctx)
 
     @Override
     public ChoiceExpr visitOption_expr_prop(KeYParser.Option_expr_propContext ctx) {
+        String category = ctx.option().cat.getText();
+        String value = ctx.option().value.getText();
+        String choiceStr = category + ":" + value;
+        /*
+         * Make sure that the choice (category and value!) is known to KeY, i.e. that it is declared
+         * in the file `optionsDeclarations.key`. This prevents from accidentally deactivating
+         * (parts of) taclets due to non-existing choices (see
+         * https://github.com/KeYProject/key/issues/3352).
+         */
+        if (choices().lookup(choiceStr) == null) {
+            semanticError(ctx, "Could not find choice: %s", category + ":" + choiceStr);
+        }
         return ChoiceExpr.variable(ctx.option().cat.getText(), ctx.option().value.getText());
     }
 

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

@@ -166,6 +166,8 @@ public Taclet generateRelationalRepresentsTaclet(Name tacletName, Term originalA
             new RewriteTacletGoalTemplate(addedSeq, ImmutableSLList.nil(), findTerm);
 
         // choices, rule set
+        // Be careful that the choices used here is actually declared (see optionsDeclarations.key),
+        // otherwise the taclet will be unusable!
         var choice = ChoiceExpr.variable("modelFields",
             satisfiabilityGuard ? "showSatisfiability" : "treatAsAxiom");
         final RuleSet ruleSet = new RuleSet(

key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java

@@ -669,11 +669,10 @@ static RewriteTaclet createTaclet(String name, Term find1, Term find2, Term goal
         assert find1.sub(0).op().name().equals(find2.sub(0).op().name());
         assert find1.sub(0).arity() == find2.sub(0).arity();
 
-        Map<ProgramVariable, ProgramVariable> map =
-            new LinkedHashMap<>();
+        Map<Operator, Operator> map = new LinkedHashMap<>();
         int i = 0;
         for (Term sub : find1.sub(0).subs()) {
-            map.put((ProgramVariable) find2.sub(0).sub(i).op(), (ProgramVariable) sub.op());
+            map.put(find2.sub(0).sub(i).op(), sub.op());
             i++;
         }
         final OpReplacer or = new OpReplacer(map, services.getTermFactory());

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key

@@ -119,7 +119,7 @@
 // --------------------------------------------------------------------------
 // Axioms defining the integer translation functions
 // --------------------------------------------------------------------------
-\rules(programRules:Java, intRules:javaSemantics) {
+\rules(programRules:Java & (intRules:javaSemantics | intRules:arithmeticSemanticsCheckingOF)) {
     expandInByte {
         \find(inByte(i))
         \replacewith(inRangeByte(i))
@@ -149,7 +149,9 @@
         \replacewith(inRangeLong(i))
         \heuristics(concrete)
     };
+}
 
+\rules(programRules:Java, intRules:javaSemantics) {
     translateJavaUnaryMinusInt {
         \find(javaUnaryMinusInt(left))
         \replacewith(unaryMinusJint(left))

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key

@@ -15,7 +15,7 @@
     \term numbers iz, jz;
 }
 
-\rules(programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF)) {
+\rules(programRules:Java & intRules:arithmeticSemanticsIgnoringOF) {
 
     // ------------------------------------------------------------------------
     // Rules to expand the predicates inByte, inShort, inInt, and inLong
@@ -50,6 +50,9 @@
         \replacewith(true)
         \heuristics(concrete)
     };
+}
+
+\rules(programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF)) {
 
     // --------------------------------------------------------------------------
     // Axioms defining the integer translation functions