From 24e26893a4c76927ca217c24289e1b11db806098 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 7 Jul 2024 15:28:52 +0200 Subject: [PATCH 1/2] remove version lock for JDT in spotless --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index bf77f3a1cf..5b51e1b46b 100644 --- a/build.gradle +++ b/build.gradle @@ -351,7 +351,7 @@ subprojects { /* At the moment, we have to ensure that version 4.22 of the eclipse formatter is run, since newer versions * of the formatter crash in SymbolicExecutionTreeBuilder (seems to be a but in the formatter)! */ - eclipse("4.22").configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml") + eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml") trimTrailingWhitespace() // not sure how to set this in the xml file ... //googleJavaFormat().aosp().reflowLongStrings() From 9a88c26f32284cabce2e5caa125c3bba0f2ade93 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 7 Jul 2024 15:32:05 +0200 Subject: [PATCH 2/2] apply spotless --- .../util/TestSymbolicExecutionUtil.java | 2 +- .../ilkd/key/macros/scripts/MacroCommand.java | 2 +- .../java/de/uka/ilkd/key/pp/LogicPrinter.java | 4 +++- ...termediatePresentationProofFileParser.java | 5 +++-- .../de/uka/ilkd/key/rule/NoPosTacletApp.java | 4 ++-- .../ilkd/key/rule/inst/SVInstantiations.java | 4 ++-- .../key/rule/metaconstruct/UnwindLoop.java | 10 ++++++++- .../jml/translation/JMLSpecFactory.java | 4 ++-- .../service/KeYCrossReferenceSourceInfo.java | 2 +- .../uka/ilkd/key/logic/TestSemisequent.java | 2 +- .../performance/DataRecordingTestFile.java | 2 +- .../key/gui/actions/SendFeedbackAction.java | 2 +- .../ilkd/key/gui/sourceview/JavaDocument.java | 3 ++- .../main/java/recoder/io/PropertyNames.java | 21 ++++++++++++++++--- .../recoder/service/DefaultSourceInfo.java | 2 +- recoder/src/main/java/recoder/util/Order.java | 3 ++- 16 files changed, 50 insertions(+), 22 deletions(-) diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java index 49a2d95a90..c445ff7b36 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java @@ -43,7 +43,7 @@ public class TestSymbolicExecutionUtil extends AbstractSymbolicExecutionTestCase public void test1ImproveReadability() throws ProblemLoaderException { File location = new File(testCaseDirectory, "/readability/InnerAndAnonymousTypeTest/InnerAndAnonymousTypeTest.java") - .getAbsoluteFile(); + .getAbsoluteFile(); assertTrue(location.exists(), "Could not find required resource: " + location); KeYEnvironment environment = KeYEnvironment.load(location, null, null, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java index 2a431b1cad..88f40a5346 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java @@ -131,7 +131,7 @@ public static PosInOccurrence extractMatchingPio(final Sequent sequent, final St for (int i = 1; i < sequent.size() + 1; i++) { final boolean matchesRegex = formatTermString( LogicPrinter.quickPrintTerm(sequent.getFormulabyNr(i).formula(), services)) - .matches(".*" + matchRegEx + ".*"); + .matches(".*" + matchRegEx + ".*"); if (matchesRegex) { if (matched) { throw new ScriptException("More than one occurrence of a matching term."); diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 11deca874c..feafcf39a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -1344,7 +1344,9 @@ public void printPostfixTerm(Term t, int ass, String name) { * the format is like * * 
-     * {@code p & q}
+     * {@code
+     * p & q
+     * }
      *
*

* The subterms are printed using {@link #printTermContinuingBlock(Term)}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index 178990cb00..c3ef8763cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -210,8 +210,9 @@ public void beginExpr(ProofElementID eid, String str) { errors.add(e); } } - case MERGE_ABSTRACTION_PREDICATES -> ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = - str; + case MERGE_ABSTRACTION_PREDICATES -> + ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = + str; case MERGE_USER_CHOICES -> ((BuiltinRuleInformation) ruleInfo).currUserChoices = str; case NOTES -> { ruleInfo.notes = str; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java index 2b6434e380..6d4838be14 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java @@ -297,8 +297,8 @@ public PosInOccurrence posInOccurrence() { * * 

      *  {@code
-     * ifFormulaInstantiations () == null &&
-     *   ( pos == null || termConstraint.isSatisfiable () )
+     * ifFormulaInstantiations() == null &&
+     *         (pos == null || termConstraint.isSatisfiable())
      * }
      *
* diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index d10a89efcd..168508fac6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -270,7 +270,7 @@ public SVInstantiations addInteresting(SchemaVariable sv, InstantiationEntry Services services) { return new SVInstantiations(map.put(sv, entry), interesting().put(sv, entry), getUpdateContext(), getGenericSortInstantiations(), getGenericSortConditions()) - .checkSorts(sv, entry, false, services); + .checkSorts(sv, entry, false, services); } @@ -653,7 +653,7 @@ public String toString() { public SVInstantiations add(GenericSortCondition p_c, Services services) throws SortException { return new SVInstantiations(map, interesting(), getUpdateContext(), getGenericSortInstantiations(), getGenericSortConditions().prepend(p_c)) - .checkCondition(p_c, false, services); + .checkCondition(p_c, false, services); } public ExecutionContext getExecutionContext() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java index e906accd69..33cf13468c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java @@ -29,7 +29,15 @@ * * 
  * {@code
- * if (i<10) l1:{ l2:{ i++; } while (i<10) { i++; } }
+ * if (i < 10)
+ *     l1: {
+ *         l2: {
+ *             i++;
+ *         }
+ *         while (i < 10) {
+ *             i++;
+ *         }
+ *     }
  * }
  *
* diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 5c65044189..a9ef73b301 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -1428,7 +1428,7 @@ public ImmutableSet createJMLLoopContracts(final IProgramMethod me clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly, clauses.diverges, clauses.assignables, clauses.assignablesFree, clauses.hasAssignable, clauses.hasFreeAssignable, clauses.decreases, services) - .create(); + .create(); } /** @@ -1463,7 +1463,7 @@ public ImmutableSet createJMLLoopContracts(IProgramMethod method, clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly, clauses.diverges, clauses.assignables, clauses.assignablesFree, clauses.hasAssignable, clauses.hasFreeAssignable, clauses.decreases, services) - .create(); + .create(); } private ProgramVariableCollection createProgramVariablesForStatement(Statement statement, diff --git a/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java b/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java index 4e18b11c1f..fa16983f5e 100644 --- a/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java +++ b/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java @@ -280,7 +280,7 @@ public Variable getVariable(String name, ProgramElement context) { */ EnumConstantSpecification ecs = (EnumConstantSpecification) ((EnumDeclaration) getType( ((Case) context.getASTParent()).getParent().getExpression())) - .getVariableInScope(name); + .getVariableInScope(name); // must not resolve! qualifying enum constant in case-statements is forbidden! return ecs; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java index 8df3490b23..64b6ea7c09 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java @@ -294,7 +294,7 @@ public void testListReplaceAddRedundantList() { // [exp.: p,q,a,b,c,r] Semisequent expected = extract(extract( extract(extract(origin.insertLast(con[4])).insertLast(con[5])).insertLast(con[6])) - .insertLast(con[2])); + .insertLast(con[2])); // insert:[a,b,c,r,r,q,p] ImmutableList insertionList = ImmutableSLList.nil().prepend(con[0]).prepend(con[1]).prepend(con[2]) diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java index 3617cbc09c..9e6a42e9e8 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java @@ -52,7 +52,7 @@ private static ApplyStrategyInfo applyStrategy(Proof proof, Strategy strategy) { proof.setActiveStrategy(strategy); return new ApplyStrategy( proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create()) - .start(proof, proof.openGoals().head()); + .start(proof, proof.openGoals().head()); } public final ProfilingDirectories getProfileDirectories() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 1193b3e540..8ddaa942b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -118,7 +118,7 @@ void appendDataToZipOutputStream(ZipOutputStream stream) throws IOException { zipEntryFileName += ".exception"; data = (e.getClass().getSimpleName() + " occured while trying to read data.\n" + e.getMessage() + "\n" + serializeStackTrace(e)) - .getBytes(StandardCharsets.UTF_8); + .getBytes(StandardCharsets.UTF_8); } stream.putNextEntry(new ZipEntry(zipEntryFileName)); stream.write(data); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index dd63b24f61..083d39d5f9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -469,7 +469,8 @@ private void processChar(char strChar) throws BadLocationException { // case '*': // case '/': - case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', '>', '=', '\'' -> + case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', + '>', '=', '\'' -> // case ' ': // case '"': // case '\'': diff --git a/recoder/src/main/java/recoder/io/PropertyNames.java b/recoder/src/main/java/recoder/io/PropertyNames.java index 338a636e44..a5c45722a2 100644 --- a/recoder/src/main/java/recoder/io/PropertyNames.java +++ b/recoder/src/main/java/recoder/io/PropertyNames.java @@ -129,7 +129,12 @@ public interface PropertyNames { * * 
      * {@code
-     * while (i < n) { if (a[i] == x) { return i; } i += 1; }
+     * while (i < n) {
+     *     if (a[i] == x) {
+     *         return i;
+     *     }
+     *     i += 1;
+     * }
      * }
      *
* @@ -138,7 +143,12 @@ public interface PropertyNames { * * 
      * {@code
-     * while (i < n) { if (a[i] == x) { return i; } i += 1; }
+     * while (i < n) {
+     *     if (a[i] == x) {
+     *         return i;
+     *     }
+     *     i += 1;
+     * }
      * }
      *
* @@ -147,7 +157,12 @@ public interface PropertyNames { * * 
      * {@code
-     * while (i < n) { if (a[i] == x) { return i; } i += 1; }
+     * while (i < n) {
+     *     if (a[i] == x) {
+     *         return i;
+     *     }
+     *     i += 1;
+     * }
      * }
      *
* diff --git a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java index 9ccb1b9707..61bf5ea293 100644 --- a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java @@ -1578,7 +1578,7 @@ public Variable getVariable(String name, ProgramElement context) { */ EnumConstantSpecification ecs = (EnumConstantSpecification) ((EnumDeclaration) getType( ((Case) context.getASTParent()).getParent().getExpression())) - .getVariableInScope(name); + .getVariableInScope(name); // must not resolve! qualifying enum constant in case-statements is forbidden! return ecs; } diff --git a/recoder/src/main/java/recoder/util/Order.java b/recoder/src/main/java/recoder/util/Order.java index 4e08c45fd0..a25f40b8e7 100644 --- a/recoder/src/main/java/recoder/util/Order.java +++ b/recoder/src/main/java/recoder/util/Order.java @@ -26,7 +26,8 @@ * * 
  * {@code
- * lessOrEquals(x,y)==(less(x,y) || equals(x,y))}
+ * lessOrEquals(x, y) == (less(x, y) || equals(x, y))
+ * }
  * ,
  *
*