Spotless & merge fixes

Author: Drodt

key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java

@@ -33,35 +33,7 @@
 import de.uka.ilkd.key.java.ast.reference.ThisReference;
 import de.uka.ilkd.key.java.ast.reference.TypeRef;
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
-import de.uka.ilkd.key.java.ast.statement.Branch;
-import de.uka.ilkd.key.java.ast.statement.Break;
-import de.uka.ilkd.key.java.ast.statement.Case;
-import de.uka.ilkd.key.java.ast.statement.Catch;
-import de.uka.ilkd.key.java.ast.statement.Continue;
-import de.uka.ilkd.key.java.ast.statement.Default;
-import de.uka.ilkd.key.java.ast.statement.Do;
-import de.uka.ilkd.key.java.ast.statement.Else;
-import de.uka.ilkd.key.java.ast.statement.EmptyStatement;
-import de.uka.ilkd.key.java.ast.statement.EnhancedFor;
-import de.uka.ilkd.key.java.ast.statement.Finally;
-import de.uka.ilkd.key.java.ast.statement.For;
-import de.uka.ilkd.key.java.ast.statement.ForUpdates;
-import de.uka.ilkd.key.java.ast.statement.Guard;
-import de.uka.ilkd.key.java.ast.statement.IForUpdates;
-import de.uka.ilkd.key.java.ast.statement.IGuard;
-import de.uka.ilkd.key.java.ast.statement.ILoopInit;
-import de.uka.ilkd.key.java.ast.statement.If;
-import de.uka.ilkd.key.java.ast.statement.LabeledStatement;
-import de.uka.ilkd.key.java.ast.statement.LoopInit;
-import de.uka.ilkd.key.java.ast.statement.MethodBodyStatement;
-import de.uka.ilkd.key.java.ast.statement.MethodFrame;
-import de.uka.ilkd.key.java.ast.statement.Return;
-import de.uka.ilkd.key.java.ast.statement.Switch;
-import de.uka.ilkd.key.java.ast.statement.SynchronizedBlock;
-import de.uka.ilkd.key.java.ast.statement.Then;
-import de.uka.ilkd.key.java.ast.statement.Throw;
-import de.uka.ilkd.key.java.ast.statement.Try;
-import de.uka.ilkd.key.java.ast.statement.While;
+import de.uka.ilkd.key.java.ast.statement.*;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.VariableNamer;
 import de.uka.ilkd.key.logic.op.IProgramMethod;

key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.PosInProgram;
 import de.uka.ilkd.key.logic.PossibleProgramPrefix;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.util.Debug;
 
 import org.key_project.util.ExtList;
@@ -143,7 +144,6 @@ public boolean equals(Object o) {
      * computes the prefix elements for the given array of statment block
      */
     public static ImmutableArray<PossibleProgramPrefix> computePrefixElements(
-            ImmutableArray<? extends Statement> b,
             PossibleProgramPrefix current) {
         final ArrayList<PossibleProgramPrefix> prefix = new ArrayList<>();
         prefix.add(current);
@@ -156,7 +156,6 @@ public static ImmutableArray<PossibleProgramPrefix> computePrefixElements(
         return new ImmutableArray<>(prefix);
     }
 
-
     /**
      * Get body.
      *

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ActiveCase.java

@@ -1,9 +1,10 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.java.statement;
+package de.uka.ilkd.key.java.ast.statement;
 
 import de.uka.ilkd.key.java.*;
+import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.PosInProgram;
 import de.uka.ilkd.key.logic.PossibleProgramPrefix;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java

@@ -9,8 +9,6 @@
 import de.uka.ilkd.key.java.ast.NonTerminalProgramElement;
 import de.uka.ilkd.key.java.ast.PositionInfo;
 
-import de.uka.ilkd.key.java.PositionInfo;
-
 import org.key_project.util.ExtList;
 
 /**

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java

@@ -81,7 +81,7 @@ public Case(ExtList children, Expression expr, PositionInfo pos) {
 
     public Case(Expression expr, ImmutableArray<Statement> body, PositionInfo pi,
             List<Comment> comments) {
-        super(pi, comments);
+        super(new ExtList(comments.toArray()), pi);
         this.expression = expr;
         this.body = body;
     }

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java

@@ -5,10 +5,7 @@
 
 import java.util.List;
 
-import de.uka.ilkd.key.java.ast.Comment;
-import de.uka.ilkd.key.java.ast.PositionInfo;
-import de.uka.ilkd.key.java.ast.ProgramElement;
-import de.uka.ilkd.key.java.ast.Statement;
+import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.visitor.Visitor;
 
 import org.key_project.util.ExtList;
@@ -56,7 +53,7 @@ public Default(ExtList children) {
     }
 
     public Default(ImmutableArray<Statement> body, PositionInfo pi, List<Comment> comments) {
-        super(pi, comments);
+        super(new ExtList(comments.toArray()), pi);
         this.body = body;
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java

@@ -5,8 +5,11 @@
 
 import java.util.List;
 
+import de.uka.ilkd.key.java.ProgramPrefixUtil;
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.expression.Expression;
+import de.uka.ilkd.key.java.ast.expression.literal.Literal;
+import de.uka.ilkd.key.java.ast.reference.MetaClassReference;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.PosInProgram;
 import de.uka.ilkd.key.logic.PossibleProgramPrefix;
@@ -118,6 +121,9 @@ public Switch(PositionInfo pi, List<Comment> c, Expression expr,
         super(pi, c);
         this.expression = expr;
         this.branches = branches;
+        ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this);
+        prefixLength = info.getLength();
+        innerMostMethodFrame = info.getInnerMostMethodFrame();
     }
 
 
@@ -292,7 +298,7 @@ public MethodFrame getInnerMostMethodFrame() {
 
     @Override
     public ImmutableArray<PossibleProgramPrefix> getPrefixElements() {
-        return StatementBlock.computePrefixElements(this);
+        return StatementBlock.computePrefixElements();
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranch.java

@@ -1,9 +1,9 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.java.statement;
+package de.uka.ilkd.key.java.ast.statement;
 
-import de.uka.ilkd.key.java.PositionInfo;
+import de.uka.ilkd.key.java.ast.PositionInfo;
 
 import org.key_project.util.ExtList;
 

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SwitchBranchSVWrapper.java

@@ -1,11 +1,11 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.java.statement;
+package de.uka.ilkd.key.java.ast.statement;
 
-import de.uka.ilkd.key.java.ProgramElement;
-import de.uka.ilkd.key.java.SourceData;
-import de.uka.ilkd.key.java.Statement;
+import de.uka.ilkd.key.java.ast.ProgramElement;
+import de.uka.ilkd.key.java.ast.SourceData;
+import de.uka.ilkd.key.java.ast.Statement;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.op.ProgramSV;
 import de.uka.ilkd.key.rule.MatchConditions;