increase spotless version (and thus also eclipse formatter) to fix missing space in instanceof formatting

Author: WolframPfeifer

build.gradle

@@ -21,7 +21,7 @@ plugins {
     // id "com.github.ben-manes.versions" version "0.39.0"
 
     // Code formatting
-    id "com.diffplug.spotless" version "6.16.0"
+    id "com.diffplug.spotless" version "6.20.0"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -335,7 +335,10 @@ subprojects {
             toggleOffOn()
 
             removeUnusedImports()
-            eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
+            /* 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")
             trimTrailingWhitespace()        // not sure how to set this in the xml file ...
             //googleJavaFormat().aosp().reflowLongStrings()
 

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java

@@ -23,7 +23,7 @@ public class ContractProofReferencesAnalyst implements IProofReferencesAnalyst {
      */
     @Override
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
-        if (node.getAppliedRuleApp()instanceof AbstractContractRuleApp contractRuleApp) {
+        if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp contractRuleApp) {
             DefaultProofReference<Contract> reference = new DefaultProofReference<>(
                 IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation());
             LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java

@@ -26,7 +26,7 @@ public class MethodBodyExpandProofReferencesAnalyst implements IProofReferencesA
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             NodeInfo info = node.getNodeInfo();
-            if (info.getActiveStatement()instanceof MethodBodyStatement mbs) {
+            if (info.getActiveStatement() instanceof MethodBodyStatement mbs) {
                 IProgramMethod pm = mbs.getProgramMethod(services);
                 DefaultProofReference<IProgramMethod> reference =
                     new DefaultProofReference<>(IProofReference.INLINE_METHOD, node,

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java

@@ -55,7 +55,7 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                         new LinkedHashSet<>();
                     result.add(reference);
                     return result;
-                } else if (info.getActiveStatement()instanceof Assignment assignment) {
+                } else if (info.getActiveStatement() instanceof Assignment assignment) {
                     ExecutionContext context = extractContext(node, services);
                     LinkedHashSet<IProofReference<?>> result =
                         new LinkedHashSet<>();
@@ -109,7 +109,7 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
             IProgramMethod pm = mr.method(services, refPrefixType, context);
             return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         } else {
-            if (!(node.getAppliedRuleApp()instanceof PosTacletApp app)) {
+            if (!(node.getAppliedRuleApp() instanceof PosTacletApp app)) {
                 throw new IllegalArgumentException("PosTacletApp expected.");
             }
             if (!"staticMethodCallStaticWithAssignmentViaTypereference"

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -175,7 +175,7 @@ protected void fillInitialObjectsToIgnoreRecursively(Term term, Set<Term> toFill
             for (int i = 0; i < term.arity(); i++) {
                 fillInitialObjectsToIgnoreRecursively(term.sub(i), toFill);
             }
-        } else if (term.op()instanceof ElementaryUpdate eu) {
+        } else if (term.op() instanceof ElementaryUpdate eu) {
             if (eu.lhs() instanceof ProgramVariable) {
                 toFill.add(term.sub(0));
             }
@@ -254,11 +254,11 @@ protected void collectLocationsFromTerm(Term updateTerm,
                 collectLocationsFromTerm(sub, locationsToFill, updateCreatedObjectsToFill,
                     updateValueObjectsToFill, objectsToIgnore);
             }
-        } else if (updateTerm.op()instanceof ElementaryUpdate eu) {
+        } else if (updateTerm.op() instanceof ElementaryUpdate eu) {
             if (SymbolicExecutionUtil.isHeapUpdate(getServices(), updateTerm)) {
                 collectLocationsFromHeapUpdate(updateTerm.sub(0), locationsToFill,
                     updateCreatedObjectsToFill, updateValueObjectsToFill);
-            } else if (eu.lhs()instanceof ProgramVariable var) {
+            } else if (eu.lhs() instanceof ProgramVariable var) {
                 final HeapLDT heapLDT = getServices().getTypeConverter().getHeapLDT();
                 if (!SymbolicExecutionUtil.isHeap(var, heapLDT)) {
                     if (!isImplicitProgramVariable(var)

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java

@@ -466,7 +466,7 @@ protected ImmutableSet<Term> extractAppliedCutsSet(Node goalnode, Node root)
         while (!(goalnode.serialNr() == root.serialNr())) {
             final Node oldNode = goalnode;
             goalnode = goalnode.parent();
-            if (goalnode.getAppliedRuleApp()instanceof NoPosTacletApp npta) {
+            if (goalnode.getAppliedRuleApp() instanceof NoPosTacletApp npta) {
                 if ("CUT".equalsIgnoreCase(npta.taclet().name().toString())) {
                     Term inst = (Term) npta.instantiations()
                             .lookupEntryForSV(new Name("cutFormula")).value().getInstantiation();

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java

@@ -253,7 +253,7 @@ private static void evaluateNode(
                         }
                     }
                 }
-            } else if (parent.getAppliedRuleApp()instanceof OneStepSimplifierRuleApp app) {
+            } else if (parent.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp app) {
                 PosInOccurrence parentPio = null;
                 for (RuleApp protocolApp : app.getProtocol()) {
                     if (parentPio != null) {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java

@@ -170,7 +170,7 @@ protected void collectRemembranceVariables(Term term,
             for (Term sub : term.subs()) {
                 collectRemembranceVariables(sub, remembranceHeaps, remembranceLocalVariables);
             }
-        } else if (term.op()instanceof ElementaryUpdate eu) {
+        } else if (term.op() instanceof ElementaryUpdate eu) {
             if (SymbolicExecutionUtil.isHeap(eu.lhs(),
                 getServices().getTypeConverter().getHeapLDT())) {
                 remembranceHeaps.put((LocationVariable) term.sub(0).op(),

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java

@@ -87,7 +87,7 @@ protected String lazyComputeName() throws ProofInputException {
         if (!isDisposed()) {
             final Services services = getServices();
             // Make sure that the contract is compatible
-            if (!(getContract()instanceof FunctionalOperationContract contract)) {
+            if (!(getContract() instanceof FunctionalOperationContract contract)) {
                 throw new ProofInputException("Unsupported contract: " + getContract());
             }
             // Compute instantiation

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java

@@ -166,7 +166,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
      * @return {@code true} is applicable, {@code false} is not applicable
      */
     private boolean isApplicableQuery(Goal goal, Term pmTerm, PosInOccurrence pio) {
-        if (pmTerm.op()instanceof IProgramMethod pm && pmTerm.freeVars().isEmpty()) {
+        if (pmTerm.op() instanceof IProgramMethod pm && pmTerm.freeVars().isEmpty()) {
             final Sort nullSort = goal.proof().getJavaInfo().nullSort();
             if (pm.isStatic()
                     || (pmTerm.sub(1).sort().extendsTrans(goal.proof().getJavaInfo().objectSort())