diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index 1365c36e398..d4bd383fc1c 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -19,10 +19,10 @@ jobs: java-version: 21 distribution: 'corretto' cache: 'gradle' + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.3.2 - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - 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/gradle-build-action@v3.3.2 with: - arguments: --continue spotlessCheck \ No newline at end of file + arguments: --continue spotlessCheck diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml index 904b5db74f9..e46dd959484 100644 --- a/.github/workflows/gradle-publish.yml +++ b/.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/setup-gradle@v3.3.2 - name: Assemble with Gradle - uses: gradle/gradle-build-action@v3.3.2 - 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/gradle-build-action@v3.3.2 - with: - arguments: publish + run: ./gradlew publish env: USERNAME: ${{ github.actor }} TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index d5dc9e44c78..82e5a48f7be 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -18,11 +18,10 @@ jobs: java-version: '21' distribution: 'corretto' cache: 'gradle' - - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: alldoc + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.3.2 + - name: Build Documentation with Gradle + run: ./gradlew alldoc - name: Package run: tar cvfj javadoc.tar.bz2 build/docs/javadoc diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 4e047eafeb2..97cd713ffac 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -30,10 +30,10 @@ jobs: java-version: 17 distribution: 'temurin' + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.3.2 - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --parallel assemble + run: ./gradlew --parallel assemble - name: Delete previous nightly release continue-on-error: true diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 250792c3a2c..360cb718d81 100644 --- a/.github/workflows/opttest.yml +++ b/.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 diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index bc34c820e96..a9f68ed0541 100644 --- a/.github/workflows/tests.yml +++ b/.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/setup-gradle@v3.3.2 - name: "Running tests: ${{ matrix.test }}" - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue ${{ matrix.test }} + run: ./gradlew --continue ${{ matrix.test }} - name: Upload test results uses: actions/upload-artifact@v4 diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml index 0d8cb6bc041..96a248d0b2c 100644 --- a/.github/workflows/tests_winmac.yml +++ b/.github/workflows/tests_winmac.yml @@ -28,10 +28,11 @@ jobs: distribution: 'corretto' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue -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 -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/setup-gradle@v3.3.2 - name: "Running tests: ${{ matrix.test }}" - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue ${{ matrix.test }} + run: ./gradlew --continue ${{ matrix.test }} - name: Upload test results uses: actions/upload-artifact@v4 diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 3e558815f71..d34c5c19a13 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/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()); } 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 4f513fef8dd..18f5c3ba079 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 @@ -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( diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java index 4ffb5121aad..175e40dd2fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java +++ b/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 map = - new LinkedHashMap<>(); + Map 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()); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key index 06d0debeb8f..a8f81a43f5e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key +++ b/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)) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key index cc46e0b99bf..0076d499167 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key +++ b/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 diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key index f0a7a3e49e9..7982511fa67 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key @@ -42,9 +42,9 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) + \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) }; \replacewith({#loc := javaMulInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -56,9 +56,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt * #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(mul(#seCharByteShortInt, #seLong))) + \add(==> inLong(mul(#seCharByteShortInt, #seLong))) }; \replacewith({#loc := javaMulLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -70,9 +70,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong * #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(mul(#seLong, #seCharByteShortInt))) + \add(==> inLong(mul(#seLong, #seCharByteShortInt))) }; \replacewith({#loc := javaMulLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -84,9 +84,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 * #seLong1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(mul(#seLong0, #seLong1))) + \add(==> inLong(mul(#seLong0, #seLong1))) }; \replacewith({#loc := javaMulLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -280,9 +280,9 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) + \add(==> inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) }; \replacewith({#loc := javaSubInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -294,9 +294,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt - #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(sub(#seCharByteShortInt, #seLong))) + \add(==> inLong(sub(#seCharByteShortInt, #seLong))) }; \replacewith({#loc := javaSubLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -308,9 +308,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong - #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(sub(#seLong, #seCharByteShortInt))) + \add(==> inLong(sub(#seLong, #seCharByteShortInt))) }; \replacewith( {#loc := javaSubLong(#seLong, #seCharByteShortInt)} @@ -323,9 +323,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 - #seLong1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(sub(#seLong0, #seLong1))) + \add(==> inLong(sub(#seLong0, #seLong1))) }; \replacewith({#loc := javaSubLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -339,9 +339,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 + #seCharByteShortInt1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) + \add(==> inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) }; \replacewith( {#loc := javaAddInt(#seCharByteShortInt0, #seCharByteShortInt1)} @@ -354,9 +354,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt + #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(add(#seCharByteShortInt, #seLong))) + \add(==> inLong(add(#seCharByteShortInt, #seLong))) }; \replacewith( {#loc := javaAddLong(#seCharByteShortInt, #seLong)} @@ -369,9 +369,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong + #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(add(#seLong, #seCharByteShortInt))) + \add(==> inLong(add(#seLong, #seCharByteShortInt))) }; \replacewith({#loc := javaAddLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -384,9 +384,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 + #seLong1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(add(#seLong0, #seLong1))) + \add(==> inLong(add(#seLong0, #seLong1))) }; \replacewith({#loc := javaAddLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -541,9 +541,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >> #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(shiftright(#seLong0, #se))) + \add(==> inInt(shiftright(#seLong0, #se))) }; \replacewith( {#loc := javaShiftRightInt(#seCharByteShortInt0, #se)} @@ -556,9 +556,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >> #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(shiftright(#seLong0, #se))) + \add(==> inInt(shiftright(#seLong0, #se))) }; \replacewith( {#loc := javaShiftRightLong(#seLong0, #se)} @@ -573,9 +573,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 << #se; ...} \endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(shiftleft(#seCharByteShortInt0, #se))) + \add(==> inInt(shiftleft(#seCharByteShortInt0, #se))) }; \replacewith( {#loc := javaShiftLeftInt(#seCharByteShortInt0, #se)} @@ -588,9 +588,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 << #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(shiftleft(#seLong0, #se))) + \add(==> inLong(shiftleft(#seLong0, #se))) }; \replacewith( {#loc := javaShiftLeftLong(#seLong0, #se)} @@ -605,9 +605,9 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >>> #se; ...} \endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) + \add(==> inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) }; \replacewith( {#loc := javaUnsignedShiftRightInt(#seCharByteShortInt0, #se)} @@ -620,9 +620,9 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >>> #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(unsignedshiftrightJlong(#seLong0, #se))) + \add(==> inLong(unsignedshiftrightJlong(#seLong0, #se))) }; \replacewith({#loc := javaUnsignedShiftRightLong(#seLong0, #se)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -638,9 +638,9 @@ \find(\modality{#normalassign}{.. #loc = - #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(neg(#seCharByteShortInt))) + \add(==> inInt(neg(#seCharByteShortInt))) }; \replacewith({#loc := javaUnaryMinusInt(#seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -652,9 +652,9 @@ \find(\modality{#normalassign}{.. #loc = - #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(neg(#seLong))) + \add(==> inLong(neg(#seLong))) }; \replacewith({#loc := javaUnaryMinusLong(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -686,9 +686,9 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seShort; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inByte(#seShort)) + \add(==> inByte(#seShort)) }; \replacewith({#loc := javaCastByte(#seShort)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -700,9 +700,9 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inByte(#seInt)) + \add(==> inByte(#seInt)) }; \replacewith({#loc := javaCastByte(#seInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -714,9 +714,9 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inByte(#seLong)) + \add(==> inByte(#seLong)) }; \replacewith({#loc := javaCastByte(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -728,9 +728,9 @@ \find(\modality{#normalassign}{.. #loc = (short) #seInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inShort(#seInt)) + \add(==> inShort(#seInt)) }; \replacewith({#loc := javaCastShort(#seInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -742,9 +742,9 @@ \find(\modality{#normalassign}{.. #loc = (short) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inShort(#seLong)) + \add(==> inShort(#seLong)) }; \replacewith({#loc := javaCastShort(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -754,9 +754,9 @@ narrowingIntCastLong { \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(#seLong)) + \add(==> inInt(#seLong)) }; \replacewith({#loc := javaCastInt(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -768,9 +768,9 @@ \find(\modality{#normalassign}{.. #loc = (char) #seByte; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seByte)) + \add(==> inChar(#seByte)) }; \replacewith( {#loc := javaCastChar(#seByte)} @@ -783,9 +783,9 @@ \find(\modality{#normalassign}{.. #loc = (char) #seShort; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seShort)) + \add(==> inChar(#seShort)) }; \replacewith( {#loc := javaCastChar(#seShort)} @@ -798,9 +798,9 @@ \find(\modality{#normalassign}{.. #loc = (char) #seInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seInt)) + \add(==> inChar(#seInt)) }; \replacewith({#loc := javaCastChar(#seInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -812,9 +812,9 @@ \find(\modality{#normalassign}{.. #loc = (char) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seLong)) + \add(==> inChar(#seLong)) }; \replacewith({#loc := javaCastChar(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java index ef079b591af..548f53b4b39 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java @@ -125,6 +125,11 @@ public static void createNewOracle() { } } + // @Test + public void createOracle() { + createNewOracle(); + } + @ParameterizedTest @MethodSource("createCases") public void testEquality(String name, String expected) { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index cda19bb7fb9..f17dc2bbc68 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Mon Dec 18 12:41:03 CET 2023 +# Date: Fri Jun 21 16:10:16 CEST 2024 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -5394,6 +5394,14 @@ defOfSeqSub { \varcond(\notFreeIn(uSub (variable), to (int term)), \notFreeIn(uSub (variable), from (int term)), \notFreeIn(uSub (variable), seq (Seq term))) \replacewith(seqDef{uSub (variable)}(from,to,any::seqGet(seq,uSub))) +Choices: sequences:on} +----------------------------------------------------- +== defOfSeqUpd (defOfSeqUpd) ========================================= +defOfSeqUpd { +\find(seqUpd(seq,idx,value)) +\varcond(\notFreeIn(uSub (variable), seq (Seq term)), \notFreeIn(uSub (variable), value (any term)), \notFreeIn(uSub (variable), idx (int term))) +\replacewith(seqDef{uSub (variable)}(Z(0(#)),seqLen(seq),if-then-else(equals(uSub,idx),value,any::seqGet(seq,uSub)))) + Choices: sequences:on} ----------------------------------------------------- == defSeq2Map (defSeq2Map) ========================================= @@ -9233,28 +9241,28 @@ expandInByte { \find(inByte(i)) \replacewith(true) \heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +Choices: (programRules:Java & intRules:arithmeticSemanticsIgnoringOF)} ----------------------------------------------------- == expandInChar (expandInChar) ========================================= expandInChar { \find(inChar(i)) \replacewith(true) \heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +Choices: (programRules:Java & intRules:arithmeticSemanticsIgnoringOF)} ----------------------------------------------------- == expandInInt (expandInInt) ========================================= expandInInt { \find(inInt(i)) \replacewith(true) \heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +Choices: (programRules:Java & intRules:arithmeticSemanticsIgnoringOF)} ----------------------------------------------------- == expandInLong (expandInLong) ========================================= expandInLong { \find(inLong(i)) \replacewith(true) \heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +Choices: (programRules:Java & intRules:arithmeticSemanticsIgnoringOF)} ----------------------------------------------------- == expandInRangeByte (expandInRangeByte) ========================================= expandInRangeByte { @@ -9296,7 +9304,7 @@ expandInShort { \find(inShort(i)) \replacewith(true) \heuristics(concrete) -Choices: (programRules:Java & (intRules:arithmeticSemanticsIgnoringOF | intRules:arithmeticSemanticsCheckingOF))} +Choices: (programRules:Java & intRules:arithmeticSemanticsIgnoringOF)} ----------------------------------------------------- == expand_addJint (expand_addJint) ========================================= expand_addJint { @@ -9686,6 +9694,13 @@ getOfSeqSubEQ { \heuristics(simplify_enlarging, no_self_application) Choices: sequences:on} ----------------------------------------------------- +== getOfSeqUpd (getOfSeqUpd) ========================================= +getOfSeqUpd { +\find(alpha::seqGet(seqUpd(seq,idx,value),jdx)) +\replacewith(if-then-else(and(and(leq(Z(0(#)),jdx),lt(jdx,seqLen(seq))),equals(idx,jdx)),alpha::cast(value),alpha::seqGet(seq,jdx))) +\heuristics(simplify_enlarging) +Choices: sequences:on} +----------------------------------------------------- == greater (greater) ========================================= greater { \find(gt(i,i0)) @@ -12117,6 +12132,13 @@ lenOfSeqSubEQ { \heuristics(find_term_not_in_assumes, simplify) Choices: sequences:on} ----------------------------------------------------- +== lenOfSeqUpd (lenOfSeqUpd) ========================================= +lenOfSeqUpd { +\find(seqLen(seqUpd(seq,idx,value))) +\replacewith(seqLen(seq)) +\heuristics(simplify) +Choices: sequences:on} +----------------------------------------------------- == lengthReplace (lengthReplace) ========================================= lengthReplace { \find(seqLen(clReplace(str,searchChar,replaceChar))) @@ -16530,6 +16552,28 @@ square_nonneg { \heuristics(simplify_int) Choices: true} ----------------------------------------------------- +== ssubsortDirect (ssubsortDirect) ========================================= +ssubsortDirect { +\find(ssubsort(alphSub::ssort,alph::ssort)) +\replacewith(true) +\heuristics(simplify) +Choices: true} +----------------------------------------------------- +== ssubsortSup (ssubsortSup) ========================================= +ssubsortSup { +\find(ssubsort(alph::ssort,alphSub::ssort)) +\varcond(\not\same(alphSub, alph)) +\replacewith(false) +\heuristics(simplify) +Choices: true} +----------------------------------------------------- +== ssubsortTop (ssubsortTop) ========================================= +ssubsortTop { +\find(ssubsort(s,anySORT)) +\replacewith(true) +\heuristics(simplify) +Choices: true} +----------------------------------------------------- == startsWith (startsWith) ========================================= startsWith { \find(clStartsWith(sourceStr,searchStr)) @@ -17025,6 +17069,13 @@ subsetWithSetMinusLeftEQ { \heuristics(simplify_enlarging) Choices: programRules:Java} ----------------------------------------------------- +== subsortTrans (subsortTrans) ========================================= +subsortTrans { +\assumes ([ssubsort(s1,s2),ssubsort(s2,s3)]==>[]) +\add [ssubsort(s1,s3)]==>[] +\heuristics(simplify_enlarging) +Choices: true} +----------------------------------------------------- == subst_to_eq (subst_to_eq) ========================================= subst_to_eq { \find(subst{u (variable)}(t,target)) diff --git a/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof index 92240d6e68e..99d0ec441cc 100644 --- a/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof +++ b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof @@ -1,8 +1,8 @@ \profile "Java Profile"; \settings // Proof-Settings-Config-File -{ - "Choice" : { +{ + "Choice" : { "JavaCard" : "JavaCard:off", "Strings" : "Strings:on", "assertions" : "assertions:safe", @@ -24,10 +24,10 @@ "wdChecks" : "wdChecks:off", "wdOperator" : "wdOperator:L" } - } + } \proofObligation // Proof-Obligation settings -{ +{ "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput", "name" : "seqSwapPreservesSeqPerm" } diff --git a/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof index 6c84c81372b..092d8ab5774 100644 --- a/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof +++ b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof @@ -1,8 +1,8 @@ \profile "Java Profile"; \settings // Proof-Settings-Config-File -{ - "Choice" : { +{ + "Choice" : { "JavaCard" : "JavaCard:off", "Strings" : "Strings:on", "assertions" : "assertions:safe", @@ -24,10 +24,10 @@ "wdChecks" : "wdChecks:off", "wdOperator" : "wdOperator:L" } - } + } \proofObligation // Proof-Obligation settings -{ +{ "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput", "name" : "seqSwapPreservesSeqPermEQ" }