diff --git a/build.gradle b/build.gradle index bf77f3a1cf3..5b51e1b46b2 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() 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 49a2d95a902..c445ff7b364 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 2a431b1cad5..88f40a5346f 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 11deca874c7..feafcf39a24 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 178990cb002..c3ef8763cc0 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 2b6434e380e..6d4838be141 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 d10a89efcd5..168508fac60 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 e906accd693..33cf13468cd 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 5c65044189b..a9ef73b301f 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 4e18b11c1f7..fa16983f5ea 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 8df3490b235..64b6ea7c097 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 3617cbc09c9..9e6a42e9e88 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 1193b3e5406..8ddaa942b20 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 dd63b24f617..083d39d5f9a 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 338a636e444..a5c45722a22 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 9ccb1b97074..61bf5ea293d 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 4e08c45fd04..a25f40b8e7c 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))
+ * }
  * ,
  *
*