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))
+ * }
* ,
*
*