spotless fixes

Author: unp1

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java

@@ -14,8 +14,8 @@
 import de.uka.ilkd.key.speclang.jml.pretranslation.*;
 import de.uka.ilkd.key.speclang.njml.PreParser;
 import de.uka.ilkd.key.speclang.translation.SLTranslationException;
-
 import de.uka.ilkd.key.util.parsing.BuildingException;
+
 import org.key_project.util.collection.ImmutableList;
 
 import com.github.javaparser.*;
@@ -147,8 +147,9 @@ public JMLTransformer(TransformationPipelineServices services) {
             throws SLTranslationException {
         NodeList<Modifier> modifiers = new NodeList<>();
         for (JMLModifier m : decl.getModifiers()) {
-            if(m.equals(JMLModifier.MODEL)) {
-                throw new BuildingException(decl.getDecl(), "Model modifier on variable declaration detected, only model fields are allowed");
+            if (m.equals(JMLModifier.MODEL)) {
+                throw new BuildingException(decl.getDecl(),
+                    "Model modifier on variable declaration detected, only model fields are allowed");
             }
 
             Modifier mod = new Modifier(m.getParserKeyword());
@@ -276,7 +277,8 @@ private void transformClassLevelComments(TypeDeclaration<?> td) throws SLTransla
                 // We might have multiple textual constructs now, because the single comment could
                 // contain multiple JML entities (e.g. method contract and ghost field declaration)
 
-                de.uka.ilkd.key.java.Position pos = de.uka.ilkd.key.java.Position.fromOneZeroBased(1, 0);
+                de.uka.ilkd.key.java.Position pos =
+                    de.uka.ilkd.key.java.Position.fromOneZeroBased(1, 0);
                 ImmutableList<TextualJMLConstruct> constructs =
                     pp.parseClassLevel(concatenatedComment, fileName, pos);
                 services.addWarnings(pp.getWarnings());
@@ -372,8 +374,7 @@ private void transformClassLevelComments(TypeDeclaration<?> td) throws SLTransla
     }
 
     private static @NonNull PreParser getPreParser() {
-        return new PreParser(
-        );
+        return new PreParser();
     }
 
     private void addClassSpec(TypeDeclaration<?> td, TextualJMLConstruct c) {
@@ -400,13 +401,14 @@ private void addLoopSpec(Node nextMember, TextualJMLLoopSpec spec) {
         specList.add(spec);
     }
 
-    private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName) throws SLTranslationException {
+    private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName)
+            throws SLTranslationException {
         PreParser io = getPreParser();
         var stmts = new ArrayList<>(blockStmt.getStatements());
         var newStmts = new ArrayList<Statement>(blockStmt.getStatements().size() * 2);
 
         final de.uka.ilkd.key.java.Position pos =
-                de.uka.ilkd.key.java.Position.fromOneZeroBased(1, 0);
+            de.uka.ilkd.key.java.Position.fromOneZeroBased(1, 0);
 
         for (int i = 0; i < stmts.size(); i++) {
             var stmt = stmts.get(i);

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java

@@ -14,7 +14,6 @@
 import org.key_project.util.collection.ImmutableList;
 
 import com.github.javaparser.JavaParser;
-import com.github.javaparser.Position;
 import com.github.javaparser.ast.CompilationUnit;
 import com.github.javaparser.ast.Modifier;
 import com.github.javaparser.ast.Node;
@@ -29,7 +28,6 @@
 import com.github.javaparser.resolution.model.SymbolReference;
 import com.github.javaparser.resolution.types.ResolvedReferenceType;
 import com.github.javaparser.resolution.types.ResolvedType;
-import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java

@@ -10,11 +10,11 @@
 import java.util.Objects;
 import java.util.Optional;
 
-import com.github.javaparser.ast.CompilationUnit;
-import com.github.javaparser.ast.Node;
 import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.util.MiscTools;
 
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.Node;
 import org.antlr.v4.runtime.IntStream;
 import org.antlr.v4.runtime.Token;
 import org.jspecify.annotations.NonNull;

key.core/src/main/java/de/uka/ilkd/key/parser/Location.java

@@ -3,20 +3,22 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.speclang.njml;
 
+import java.net.URI;
+import java.util.ArrayList;
+import java.util.List;
+
 import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.speclang.PositionedString;
 import de.uka.ilkd.key.speclang.jml.pretranslation.JMLModifier;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLModifierList;
-import org.antlr.v4.runtime.ParserRuleContext;
-import org.jspecify.annotations.Nullable;
+
 import org.key_project.util.collection.ImmutableList;
 
-import java.net.URI;
-import java.util.ArrayList;
-import java.util.List;
+import org.antlr.v4.runtime.ParserRuleContext;
+import org.jspecify.annotations.Nullable;
 
 /**
  * Transforms pure text comments into {@link TextualJMLConstruct}s.

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/PreParser.java

@@ -6,7 +6,6 @@
 
 import de.uka.ilkd.key.parser.Location;
 
-import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
 /**
@@ -21,5 +20,6 @@ public interface HasLocation {
      *
      * @return the location of the exception
      */
-    @Nullable Location getLocation();
+    @Nullable
+    Location getLocation();
 }

key.core/src/main/java/de/uka/ilkd/key/util/parsing/HasLocation.java

@@ -63,10 +63,13 @@ public void testTypeNotInInnerScopeShouldNotBeFound() {
     public void testNestedMethodFrameRedirects() {
         try {
             HelperClassForTests.parseThrowException(
-                        testpath.resolve("typeResolutionInNestedMethodFrameResolvable.key"));
+                testpath.resolve("typeResolutionInNestedMethodFrameResolvable.key"));
         } catch (Throwable t) {
-            Assertions.fail("Resolution of type TestJavaCardDLExtensions should be successful as it is enclosed by the outer method frame " +
-                    "which redirects the scope to package sub1. Class Third should be resolvable (and visible) as the inner method-frame redirects to package sub2." +
+            Assertions.fail(
+                "Resolution of type TestJavaCardDLExtensions should be successful as it is enclosed by the outer method frame "
+                    +
+                    "which redirects the scope to package sub1. Class Third should be resolvable (and visible) as the inner method-frame redirects to package sub2."
+                    +
                     "\n\n" + t);
         }