apply spotless

KeYProject · Nov 22, 2024 · e3b5cc1 · e3b5cc1
1 parent 19263bd
commit e3b5cc1
Show file tree

Hide file tree

Showing 16 changed files with 50 additions and 22 deletions.
diff --git a/...test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/...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
@@ -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
@@ -1344,7 +1344,9 @@ public void printPostfixTerm(Term t, int ass, String name) {
      * the format is like
      *
      * <pre>
-     * {@code p & q}
+     * {@code
+     * p & q
+     * }
      * </pre>
      * <p>
      * 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
@@ -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
@@ -297,8 +297,8 @@ public PosInOccurrence posInOccurrence() {
      *
      * <pre>
      *  {@code
-     * ifFormulaInstantiations () == null &&
-     *   ( pos == null || termConstraint.isSatisfiable () )
+     * ifFormulaInstantiations() == null &&
+     *         (pos == null || termConstraint.isSatisfiable())
      * }
      * </pre>
      *

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
@@ -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
@@ -29,7 +29,15 @@
  *
  * <pre>
  * {@code
- * if (i<10) l1:{ l2:{ i++; } while (i<10) { i++; } }
+ * if (i < 10)
+ *     l1: {
+ *         l2: {
+ *             i++;
+ *         }
+ *         while (i < 10) {
+ *             i++;
+ *         }
+ *     }
  * }
  * </pre>
  *

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
@@ -1428,7 +1428,7 @@ public ImmutableSet<LoopContract> 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<LoopContract> 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
@@ -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
@@ -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<SequentFormula> insertionList =
             ImmutableSLList.<SequentFormula>nil().prepend(con[0]).prepend(con[1]).prepend(con[2])

diff --git a/...e/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java b/...e/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
@@ -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
@@ -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
@@ -129,7 +129,12 @@ public interface PropertyNames {
      *
      * <PRE>
      * {@code
-     * while (i < n) { if (a[i] == x) { return i; } i += 1; }
+     * while (i < n) {
+     *     if (a[i] == x) {
+     *         return i;
+     *     }
+     *     i += 1;
+     * }
      * }
      * </PRE>
      *
@@ -138,7 +143,12 @@ public interface PropertyNames {
      *
      * <PRE>
      * {@code
-     * while (i < n) { if (a[i] == x) { return i; } i += 1; }
+     * while (i < n) {
+     *     if (a[i] == x) {
+     *         return i;
+     *     }
+     *     i += 1;
+     * }
      * }
      * </PRE>
      *
@@ -147,7 +157,12 @@ public interface PropertyNames {
      *
      * <PRE>
      * {@code
-     * while (i < n) { if (a[i] == x) { return i; } i += 1; }
+     * while (i < n) {
+     *     if (a[i] == x) {
+     *         return i;
+     *     }
+     *     i += 1;
+     * }
      * }
      * </PRE>
      *

diff --git 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
@@ -26,7 +26,8 @@
  *
  * <pre>
  * {@code
- * lessOrEquals(x,y)==(less(x,y) || equals(x,y))}
+ * lessOrEquals(x, y) == (less(x, y) || equals(x, y))
+ * }
  * ,
  * </pre>
  *