From 5b68afc60c2499cc6b326dd8b417347994d0d735 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 15 Nov 2023 22:11:35 +0100 Subject: [PATCH 01/10] fix creating of branches for overflow checking --- .../rules/integerAssignment2UpdateRules.key | 60 +++++++++---------- 1 file changed, 30 insertions(+), 30 deletions(-) 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..190305bbd99 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,7 +42,7 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 * #seCharByteShortInt1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) }; @@ -56,7 +56,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt * #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(mul(#seCharByteShortInt, #seLong))) }; @@ -70,7 +70,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong * #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(mul(#seLong, #seCharByteShortInt))) }; @@ -84,7 +84,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 * #seLong1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(mul(#seLong0, #seLong1))) }; @@ -280,7 +280,7 @@ \find(\modality{#normalassign}{.. #loc = #seCharByteShortInt0 - #seCharByteShortInt1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) }; @@ -294,7 +294,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt - #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(sub(#seCharByteShortInt, #seLong))) }; @@ -308,7 +308,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong - #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(sub(#seLong, #seCharByteShortInt))) }; @@ -323,7 +323,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 - #seLong1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(sub(#seLong0, #seLong1))) }; @@ -339,7 +339,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 + #seCharByteShortInt1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) }; @@ -354,7 +354,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt + #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(add(#seCharByteShortInt, #seLong))) }; @@ -369,7 +369,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong + #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(add(#seLong, #seCharByteShortInt))) }; @@ -384,7 +384,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 + #seLong1; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(add(#seLong0, #seLong1))) }; @@ -541,7 +541,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >> #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(shiftright(#seLong0, #se))) }; @@ -556,7 +556,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >> #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(shiftright(#seLong0, #se))) }; @@ -573,7 +573,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 << #se; ...} \endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(shiftleft(#seCharByteShortInt0, #se))) }; @@ -588,7 +588,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 << #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(shiftleft(#seLong0, #se))) }; @@ -605,7 +605,7 @@ \find(\modality{#normalassign}{.. #loc=#seCharByteShortInt0 >>> #se; ...} \endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) }; @@ -620,7 +620,7 @@ \find(\modality{#normalassign}{.. #loc=#seLong0 >>> #se; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(unsignedshiftrightJlong(#seLong0, #se))) }; @@ -638,7 +638,7 @@ \find(\modality{#normalassign}{.. #loc = - #seCharByteShortInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(neg(#seCharByteShortInt))) }; @@ -652,7 +652,7 @@ \find(\modality{#normalassign}{.. #loc = - #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inLong(neg(#seLong))) }; @@ -686,7 +686,7 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seShort; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inByte(#seShort)) }; @@ -700,7 +700,7 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inByte(#seInt)) }; @@ -714,7 +714,7 @@ \find(\modality{#normalassign}{.. #loc = (byte) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inByte(#seLong)) }; @@ -728,7 +728,7 @@ \find(\modality{#normalassign}{.. #loc = (short) #seInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inShort(#seInt)) }; @@ -742,7 +742,7 @@ \find(\modality{#normalassign}{.. #loc = (short) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inShort(#seLong)) }; @@ -754,7 +754,7 @@ narrowingIntCastLong { \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inInt(#seLong)) }; @@ -768,7 +768,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seByte; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inChar(#seByte)) }; @@ -783,7 +783,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seShort; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inChar(#seShort)) }; @@ -798,7 +798,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seInt; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inChar(#seInt)) }; @@ -812,7 +812,7 @@ \find(\modality{#normalassign}{.. #loc = (char) #seLong; ...}\endmodality (post)) - (intRules:checkedOverflow) { + (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": \replacewith(inChar(#seLong)) }; From b301337697951cfc1e39f9afb22b026e23e01cad Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 15 Nov 2023 22:29:23 +0100 Subject: [PATCH 02/10] correct inRange(..) predicates for overflow check semantics --- .../de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key | 4 +++- .../uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key | 5 ++++- 2 files changed, 7 insertions(+), 2 deletions(-) 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 From f8d0956eb3260dd58239c2b2f93bdc2c6a9b9f7f Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 14 Feb 2024 18:34:11 +0100 Subject: [PATCH 03/10] throw an error if choices used in a taclet are not declared --- .../de/uka/ilkd/key/nparser/builder/TacletPBuilder.java | 9 +++++++++ .../uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java | 2 ++ 2 files changed, 11 insertions(+) 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 f58f7a4615f..57a6c570d75 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 @@ -595,6 +595,15 @@ 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. 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 7b8c1d045e3..09e373dbda0 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 @@ -163,6 +163,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( From 6c0875ca015d0e6bc571bd77b35c632a8006b11a Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Thu, 20 Jun 2024 04:51:16 +0200 Subject: [PATCH 04/10] Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable --- .../java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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()); From 2cb24766332aeb593635e10d0f55f361ed702c1c Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 21 Jun 2024 13:20:10 +0200 Subject: [PATCH 05/10] spotless --- .../de/uka/ilkd/key/nparser/builder/TacletPBuilder.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 7b98627be79..e6bd5534e67 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 @@ -684,9 +684,11 @@ 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. This prevents from + /* + * Make sure that the choice (category and value!) is known to KeY. This prevents from * accidentally deactivating (parts of) taclets due to non-existing choices (see - * https://github.com/KeYProject/key/issues/3352). */ + * https://github.com/KeYProject/key/issues/3352). + */ if (choices().lookup(choiceStr) == null) { semanticError(ctx, "Could not find choice: %s", category + ":" + choiceStr); } From ebfb642471efc945b9d3753bf42efe126b1fb071 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 21 Jun 2024 15:03:51 +0200 Subject: [PATCH 06/10] repair soundness of assignment2UpdateRules with checked overflows --- .../rules/integerAssignment2UpdateRules.key | 60 +++++++++---------- 1 file changed, 30 insertions(+), 30 deletions(-) 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 190305bbd99..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 @@ -44,7 +44,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) + \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1))) }; \replacewith({#loc := javaMulInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -58,7 +58,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(mul(#seCharByteShortInt, #seLong))) + \add(==> inLong(mul(#seCharByteShortInt, #seLong))) }; \replacewith({#loc := javaMulLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -72,7 +72,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(mul(#seLong, #seCharByteShortInt))) + \add(==> inLong(mul(#seLong, #seCharByteShortInt))) }; \replacewith({#loc := javaMulLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -86,7 +86,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(mul(#seLong0, #seLong1))) + \add(==> inLong(mul(#seLong0, #seLong1))) }; \replacewith({#loc := javaMulLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -282,7 +282,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) + \add(==> inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1))) }; \replacewith({#loc := javaSubInt(#seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -296,7 +296,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(sub(#seCharByteShortInt, #seLong))) + \add(==> inLong(sub(#seCharByteShortInt, #seLong))) }; \replacewith({#loc := javaSubLong(#seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -310,7 +310,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(sub(#seLong, #seCharByteShortInt))) + \add(==> inLong(sub(#seLong, #seCharByteShortInt))) }; \replacewith( {#loc := javaSubLong(#seLong, #seCharByteShortInt)} @@ -325,7 +325,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(sub(#seLong0, #seLong1))) + \add(==> inLong(sub(#seLong0, #seLong1))) }; \replacewith({#loc := javaSubLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -341,7 +341,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) + \add(==> inInt(add(#seCharByteShortInt0, #seCharByteShortInt1))) }; \replacewith( {#loc := javaAddInt(#seCharByteShortInt0, #seCharByteShortInt1)} @@ -356,7 +356,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(add(#seCharByteShortInt, #seLong))) + \add(==> inLong(add(#seCharByteShortInt, #seLong))) }; \replacewith( {#loc := javaAddLong(#seCharByteShortInt, #seLong)} @@ -371,7 +371,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(add(#seLong, #seCharByteShortInt))) + \add(==> inLong(add(#seLong, #seCharByteShortInt))) }; \replacewith({#loc := javaAddLong(#seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -386,7 +386,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(add(#seLong0, #seLong1))) + \add(==> inLong(add(#seLong0, #seLong1))) }; \replacewith({#loc := javaAddLong(#seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -543,7 +543,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(shiftright(#seLong0, #se))) + \add(==> inInt(shiftright(#seLong0, #se))) }; \replacewith( {#loc := javaShiftRightInt(#seCharByteShortInt0, #se)} @@ -558,7 +558,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(shiftright(#seLong0, #se))) + \add(==> inInt(shiftright(#seLong0, #se))) }; \replacewith( {#loc := javaShiftRightLong(#seLong0, #se)} @@ -575,7 +575,7 @@ \endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(shiftleft(#seCharByteShortInt0, #se))) + \add(==> inInt(shiftleft(#seCharByteShortInt0, #se))) }; \replacewith( {#loc := javaShiftLeftInt(#seCharByteShortInt0, #se)} @@ -590,7 +590,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(shiftleft(#seLong0, #se))) + \add(==> inLong(shiftleft(#seLong0, #se))) }; \replacewith( {#loc := javaShiftLeftLong(#seLong0, #se)} @@ -607,7 +607,7 @@ \endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) + \add(==> inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se))) }; \replacewith( {#loc := javaUnsignedShiftRightInt(#seCharByteShortInt0, #se)} @@ -622,7 +622,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(unsignedshiftrightJlong(#seLong0, #se))) + \add(==> inLong(unsignedshiftrightJlong(#seLong0, #se))) }; \replacewith({#loc := javaUnsignedShiftRightLong(#seLong0, #se)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -640,7 +640,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(neg(#seCharByteShortInt))) + \add(==> inInt(neg(#seCharByteShortInt))) }; \replacewith({#loc := javaUnaryMinusInt(#seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -654,7 +654,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inLong(neg(#seLong))) + \add(==> inLong(neg(#seLong))) }; \replacewith({#loc := javaUnaryMinusLong(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -688,7 +688,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inByte(#seShort)) + \add(==> inByte(#seShort)) }; \replacewith({#loc := javaCastByte(#seShort)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -702,7 +702,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inByte(#seInt)) + \add(==> inByte(#seInt)) }; \replacewith({#loc := javaCastByte(#seInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -716,7 +716,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inByte(#seLong)) + \add(==> inByte(#seLong)) }; \replacewith({#loc := javaCastByte(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -730,7 +730,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inShort(#seInt)) + \add(==> inShort(#seInt)) }; \replacewith({#loc := javaCastShort(#seInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -744,7 +744,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inShort(#seLong)) + \add(==> inShort(#seLong)) }; \replacewith({#loc := javaCastShort(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -756,7 +756,7 @@ \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inInt(#seLong)) + \add(==> inInt(#seLong)) }; \replacewith({#loc := javaCastInt(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -770,7 +770,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seByte)) + \add(==> inChar(#seByte)) }; \replacewith( {#loc := javaCastChar(#seByte)} @@ -785,7 +785,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seShort)) + \add(==> inChar(#seShort)) }; \replacewith( {#loc := javaCastChar(#seShort)} @@ -800,7 +800,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seInt)) + \add(==> inChar(#seInt)) }; \replacewith({#loc := javaCastChar(#seInt)} \modality{#normalassign}{.. ...}\endmodality (post)) @@ -814,7 +814,7 @@ ...}\endmodality (post)) (intRules:arithmeticSemanticsCheckingOF) { "Overflow check": - \replacewith(inChar(#seLong)) + \add(==> inChar(#seLong)) }; \replacewith({#loc := javaCastChar(#seLong)} \modality{#normalassign}{.. ...}\endmodality (post)) From 7df32919abc871e595eb00e986c8d2bb8a52adaa Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 14 Jun 2024 09:14:56 +0200 Subject: [PATCH 07/10] change gradle github action to new syntax --- .github/workflows/code_quality.yml | 31 ++++++++++++++-------------- .github/workflows/gradle-publish.yml | 10 ++++----- .github/workflows/javadoc.yml | 9 ++++---- .github/workflows/nightlydeploy.yml | 6 +++--- .github/workflows/opttest.yml | 8 +++---- .github/workflows/tests.yml | 15 +++++++------- .github/workflows/tests_winmac.yml | 15 +++++++------- 7 files changed, 45 insertions(+), 49 deletions(-) diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index 5410a014e96..a13aecf615f 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 qodana: @@ -48,10 +48,10 @@ jobs: distribution: 'corretto' java-version: '21' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue spotlessCheck + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.3.2 + - name: SpotlessCheck + run: ./gradlew --continue spotlessCheck # checkstyle: # runs-on: ubuntu-latest @@ -80,11 +80,10 @@ jobs: distribution: 'corretto' java-version: '21' cache: 'gradle' - - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue checkstyleMainChanged + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.3.2 + - name: Checkstyle + run: ./gradlew --continue checkstyleMainChanged - run: | npx violations-command-line -sarif sarif-report.json \ -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle" @@ -108,10 +107,10 @@ jobs: distribution: 'corretto' java-version: '21' cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue pmdMainChanged + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v3.3.2 + - name: PMD checks + run: ./gradlew --continue pmdMainChanged # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml 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 From f2ddbd6ee1742f32a1d7687ac10422b5cd8839ae Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Mon, 24 Jun 2024 11:35:57 +0200 Subject: [PATCH 08/10] update oracle for taclet equality test --- .../ilkd/key/nparser/TestTacletEquality.java | 6 ++ .../de/uka/ilkd/key/nparser/taclets.old.txt | 63 +++++++++++++++++-- 2 files changed, 63 insertions(+), 6 deletions(-) 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..67afa30a721 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 @@ -25,6 +25,7 @@ import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; @@ -125,6 +126,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..43b6fe9b43f 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)) From ec65160c32a0773b73913a9a87b79ce0d96d09fb Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Mon, 24 Jun 2024 11:58:28 +0200 Subject: [PATCH 09/10] spotless --- .../test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java | 1 - 1 file changed, 1 deletion(-) 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 67afa30a721..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 @@ -25,7 +25,6 @@ import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.BeforeAll; -import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; From fb3a5b12c25d771c690c6604fbfe9944ce81da51 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer <94171076+WolframPfeifer@users.noreply.github.com> Date: Mon, 24 Jun 2024 14:11:56 +0200 Subject: [PATCH 10/10] Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java More concrete comment where to declare taclet options --- .../java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 e6bd5534e67..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 @@ -685,8 +685,9 @@ public ChoiceExpr visitOption_expr_prop(KeYParser.Option_expr_propContext ctx) { String value = ctx.option().value.getText(); String choiceStr = category + ":" + value; /* - * Make sure that the choice (category and value!) is known to KeY. This prevents from - * accidentally deactivating (parts of) taclets due to non-existing choices (see + * 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) {