spotless and merge errors

Author: wadoon

key.core.example/src/main/java/org/key_project/Main.java

@@ -131,7 +131,8 @@ private static List<Contract> getContracts(KeYEnvironment<?> env) {
      * @param env the {@link KeYEnvironment} in which to prove the contract
      * @param contract the {@link Contract} to be proven
      */
-    private static void proveContract(KeYEnvironment<?> env, Contract contract) throws InterruptedException {
+    private static void proveContract(KeYEnvironment<?> env, Contract contract)
+            throws InterruptedException {
         Proof proof = null;
         try {
             // Create proof

key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java

@@ -564,7 +564,8 @@ public void startAndWaitForAutoMode(Proof proof) throws InterruptedException {
      * {@inheritDoc}
      */
     @Override
-    public void startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals) throws InterruptedException {
+    public void startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals)
+            throws InterruptedException {
         startAutoMode(proof, goals);
         waitWhileAutoMode();
     }

key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java

@@ -3,6 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.control;
 
+import java.util.concurrent.locks.Condition;
+import java.util.concurrent.locks.ReentrantLock;
+
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
@@ -16,10 +19,8 @@
 import de.uka.ilkd.key.prover.impl.ApplyStrategy;
 import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo;
 import de.uka.ilkd.key.util.ProofStarter;
-import org.key_project.util.collection.ImmutableList;
 
-import java.util.concurrent.locks.Condition;
-import java.util.concurrent.locks.ReentrantLock;
+import org.key_project.util.collection.ImmutableList;
 
 /**
  * The default implementation of {@link ProofControl}.
@@ -45,34 +46,34 @@ public class DefaultProofControl extends AbstractProofControl {
     /**
      * Constructor.
      *
-     * @param ui                        The {@link UserInterfaceControl} in which this {@link ProofControl} is used.
+     * @param ui The {@link UserInterfaceControl} in which this {@link ProofControl} is used.
      * @param defaultProverTaskListener The default {@link ProverTaskListener} which will be added
-     *                                  to all started {@link ApplyStrategy} instances.
+     *        to all started {@link ApplyStrategy} instances.
      */
     public DefaultProofControl(UserInterfaceControl ui,
-                               DefaultUserInterfaceControl defaultProverTaskListener) {
+            DefaultUserInterfaceControl defaultProverTaskListener) {
         super(defaultProverTaskListener);
         this.ui = ui;
     }
 
     /**
      * Constructor.
      *
-     * @param ui                        The {@link UserInterfaceControl} in which this {@link ProofControl} is used.
+     * @param ui The {@link UserInterfaceControl} in which this {@link ProofControl} is used.
      * @param defaultProverTaskListener The default {@link ProverTaskListener} which will be added
-     *                                  to all started {@link ApplyStrategy} instances.
-     * @param ruleCompletionHandler     An optional {@link RuleCompletionHandler}.
+     *        to all started {@link ApplyStrategy} instances.
+     * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
      */
     public DefaultProofControl(UserInterfaceControl ui,
-                               DefaultUserInterfaceControl defaultProverTaskListener,
-                               RuleCompletionHandler ruleCompletionHandler) {
+            DefaultUserInterfaceControl defaultProverTaskListener,
+            RuleCompletionHandler ruleCompletionHandler) {
         super(defaultProverTaskListener, ruleCompletionHandler);
         this.ui = ui;
     }
 
     @Override
     public synchronized void startAutoMode(Proof proof, ImmutableList<Goal> goals,
-                                           ProverTaskListener ptl) {
+            ProverTaskListener ptl) {
         if (!isInAutoMode()) {
             autoModeThread = new AutoModeThread(proof, goals, ptl);
             autoModeThread.start();
@@ -121,7 +122,7 @@ public void run() {
                 fireAutoModeStarted(new ProofEvent(proof));
                 ProofStarter starter = ptl != null
                         ? new ProofStarter(
-                        new CompositePTListener(getDefaultProverTaskListener(), ptl), false)
+                            new CompositePTListener(getDefaultProverTaskListener(), ptl), false)
                         : new ProofStarter(getDefaultProverTaskListener(), false);
                 starter.init(proof);
                 if (goals != null) {

key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java

@@ -3,6 +3,10 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.control;
 
+import java.io.File;
+import java.util.*;
+import java.util.function.Consumer;
+
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
@@ -21,11 +25,8 @@
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.util.KeYTypeUtil;
 import de.uka.ilkd.key.util.Pair;
-import org.key_project.util.collection.ImmutableSet;
 
-import java.io.File;
-import java.util.*;
-import java.util.function.Consumer;
+import org.key_project.util.collection.ImmutableSet;
 
 /**
  * Instances of this class are used to collect and access all relevant information for verification
@@ -67,7 +68,7 @@ public class KeYEnvironment<U extends UserInterfaceControl> {
     /**
      * Constructor
      *
-     * @param ui         The {@link UserInterfaceControl} in which the {@link Proof} is loaded.
+     * @param ui The {@link UserInterfaceControl} in which the {@link Proof} is loaded.
      * @param initConfig The loaded project.
      */
     public KeYEnvironment(U ui, InitConfig initConfig) {
@@ -77,11 +78,11 @@ public KeYEnvironment(U ui, InitConfig initConfig) {
     /**
      * Constructor
      *
-     * @param ui         The {@link UserInterfaceControl} in which the {@link Proof} is loaded.
+     * @param ui The {@link UserInterfaceControl} in which the {@link Proof} is loaded.
      * @param initConfig The loaded project.
      */
     public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof,
-                          Pair<String, Location> proofScript, ReplayResult replayResult) {
+            Pair<String, Location> proofScript, ReplayResult replayResult) {
         this.ui = ui;
         this.initConfig = initConfig;
         this.loadedProof = loadedProof;
@@ -180,15 +181,15 @@ public Proof createProof(ProofOblInput input) throws ProofInputException {
      * Loads the given location and returns all required references as {@link KeYEnvironment}. The
      * {@code MainWindow} is not involved in the whole process.
      *
-     * @param location      The location to load.
-     * @param classPaths    The class path entries to use.
+     * @param location The location to load.
+     * @param classPaths The class path entries to use.
      * @param bootClassPath The boot class path to use.
-     * @param includes      Optional includes to consider.
+     * @param includes Optional includes to consider.
      * @return The {@link KeYEnvironment} which contains all references to the loaded location.
      * @throws ProblemLoaderException Occurred Exception
      */
     public static KeYEnvironment<DefaultUserInterfaceControl> load(File location,
-                                                                   List<File> classPaths, File bootClassPath, List<File> includes)
+            List<File> classPaths, File bootClassPath, List<File> includes)
             throws ProblemLoaderException {
         return load(null, location, classPaths, bootClassPath, includes, false);
     }
@@ -197,103 +198,103 @@ public static KeYEnvironment<DefaultUserInterfaceControl> load(File location,
      * Loads the given location and returns all required references as {@link KeYEnvironment}. The
      * {@code MainWindow} is not involved in the whole process.
      *
-     * @param location              The location to load.
-     * @param classPaths            The class path entries to use.
-     * @param bootClassPath         The boot class path to use.
-     * @param includes              Optional includes to consider.
+     * @param location The location to load.
+     * @param classPaths The class path entries to use.
+     * @param bootClassPath The boot class path to use.
+     * @param includes Optional includes to consider.
      * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
      * @return The {@link KeYEnvironment} which contains all references to the loaded location.
      * @throws ProblemLoaderException Occurred Exception
      */
     public static KeYEnvironment<DefaultUserInterfaceControl> load(File location,
-                                                                   List<File> classPaths, File bootClassPath, List<File> includes,
-                                                                   RuleCompletionHandler ruleCompletionHandler) throws ProblemLoaderException {
+            List<File> classPaths, File bootClassPath, List<File> includes,
+            RuleCompletionHandler ruleCompletionHandler) throws ProblemLoaderException {
         return load(null, location, classPaths, bootClassPath, includes, null,
-                ruleCompletionHandler, false);
+            ruleCompletionHandler, false);
     }
 
     /**
      * Loads the given location and returns all required references as {@link KeYEnvironment}. The
      * {@code MainWindow} is not involved in the whole process.
      *
-     * @param profile                    The {@link Profile} to use.
-     * @param location                   The location to load.
-     * @param classPaths                 The class path entries to use.
-     * @param bootClassPath              The boot class path to use.
-     * @param includes                   Optional includes to consider.
+     * @param profile The {@link Profile} to use.
+     * @param location The location to load.
+     * @param classPaths The class path entries to use.
+     * @param bootClassPath The boot class path to use.
+     * @param includes Optional includes to consider.
      * @param forceNewProfileOfNewProofs {@code} true
      *        {@code AbstractProblemLoader.profileOfNewProofs} will be used as
-     *                                   {@link Profile} of new proofs, {@code false} {@link Profile} specified by problem file
-     *                                   will be used for new proofs.
+     *        {@link Profile} of new proofs, {@code false} {@link Profile} specified by problem file
+     *        will be used for new proofs.
      * @return The {@link KeYEnvironment} which contains all references to the loaded location.
      * @throws ProblemLoaderException Occurred Exception
      */
     public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, File location,
-                                                                   List<File> classPaths, File bootClassPath, List<File> includes,
-                                                                   boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
+            List<File> classPaths, File bootClassPath, List<File> includes,
+            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
         return load(profile, location, classPaths, bootClassPath, includes, null, null,
-                forceNewProfileOfNewProofs);
+            forceNewProfileOfNewProofs);
     }
 
     /**
      * Loads the given location and returns all required references as {@link KeYEnvironment}. The
      * {@code MainWindow} is not involved in the whole process.
      *
-     * @param profile                    The {@link Profile} to use.
-     * @param location                   The location to load.
-     * @param classPaths                 The class path entries to use.
-     * @param bootClassPath              The boot class path to use.
-     * @param includes                   Optional includes to consider.
-     * @param poPropertiesToForce        Some optional PO {@link Properties} to force.
-     * @param ruleCompletionHandler      An optional {@link RuleCompletionHandler}.
+     * @param profile The {@link Profile} to use.
+     * @param location The location to load.
+     * @param classPaths The class path entries to use.
+     * @param bootClassPath The boot class path to use.
+     * @param includes Optional includes to consider.
+     * @param poPropertiesToForce Some optional PO {@link Properties} to force.
+     * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
      * @param forceNewProfileOfNewProofs {@code} true
      *        {@code AbstractProblemLoader.profileOfNewProofs} will be used as {@link Profile} of
-     *                                   new proofs, {@code false} {@link Profile} specified by problem file will be used for
-     *                                   new proofs.
+     *        new proofs, {@code false} {@link Profile} specified by problem file will be used for
+     *        new proofs.
      * @return The {@link KeYEnvironment} which contains all references to the loaded location.
      * @throws ProblemLoaderException Occurred Exception
      */
     public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, File location,
-                                                                   List<File> classPaths, File bootClassPath, List<File> includes,
-                                                                   Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
-                                                                   boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
+            List<File> classPaths, File bootClassPath, List<File> includes,
+            Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
+            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
         return load(profile, location, classPaths, bootClassPath, includes, poPropertiesToForce,
-                ruleCompletionHandler,
-                null, forceNewProfileOfNewProofs);
+            ruleCompletionHandler,
+            null, forceNewProfileOfNewProofs);
     }
 
     /**
      * Loads the given location and returns all required references as {@link KeYEnvironment}. The
      * {@code MainWindow} is not involved in the whole process.
      *
-     * @param profile                    The {@link Profile} to use.
-     * @param location                   The location to load.
-     * @param classPaths                 The class path entries to use.
-     * @param bootClassPath              The boot class path to use.
-     * @param includes                   Optional includes to consider.
-     * @param poPropertiesToForce        Some optional PO {@link Properties} to force.
-     * @param ruleCompletionHandler      An optional {@link RuleCompletionHandler}.
-     * @param callbackProofLoaded        An optional callback (called when the proof is loaded, before
-     *                                   replay)
+     * @param profile The {@link Profile} to use.
+     * @param location The location to load.
+     * @param classPaths The class path entries to use.
+     * @param bootClassPath The boot class path to use.
+     * @param includes Optional includes to consider.
+     * @param poPropertiesToForce Some optional PO {@link Properties} to force.
+     * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
+     * @param callbackProofLoaded An optional callback (called when the proof is loaded, before
+     *        replay)
      * @param forceNewProfileOfNewProofs {@code} true
      *        {@code AbstractProblemLoader.profileOfNewProofs} will be used as {@link Profile} of
-     *                                   new proofs, {@code false} {@link Profile} specified by problem file will be used for
-     *                                   new proofs.
+     *        new proofs, {@code false} {@link Profile} specified by problem file will be used for
+     *        new proofs.
      * @return The {@link KeYEnvironment} which contains all references to the loaded location.
      * @throws ProblemLoaderException Occurred Exception
      */
     public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, File location,
-                                                                   List<File> classPaths, File bootClassPath, List<File> includes,
-                                                                   Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
-                                                                   Consumer<Proof> callbackProofLoaded,
-                                                                   boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
+            List<File> classPaths, File bootClassPath, List<File> includes,
+            Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
+            Consumer<Proof> callbackProofLoaded,
+            boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
         DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(ruleCompletionHandler);
         AbstractProblemLoader loader = ui.load(profile, location, classPaths, bootClassPath,
-                includes, poPropertiesToForce, forceNewProfileOfNewProofs, callbackProofLoaded);
+            includes, poPropertiesToForce, forceNewProfileOfNewProofs, callbackProofLoaded);
         InitConfig initConfig = loader.getInitConfig();
 
         return new KeYEnvironment<>(ui, initConfig, loader.getProof(),
-                loader.getProofScript(), loader.getResult());
+            loader.getProofScript(), loader.getResult());
     }
 
     public static KeYEnvironment<DefaultUserInterfaceControl> load(File keyFile)
@@ -335,9 +336,11 @@ public List<Contract> getAvailableContracts() {
         Set<KeYJavaType> kjts = getJavaInfo().getAllKeYJavaTypes();
         for (KeYJavaType type : kjts) {
             if (!KeYTypeUtil.isLibraryClass(type)) {
-                ImmutableSet<IObserverFunction> targets = getSpecificationRepository().getContractTargets(type);
+                ImmutableSet<IObserverFunction> targets =
+                    getSpecificationRepository().getContractTargets(type);
                 for (IObserverFunction target : targets) {
-                    ImmutableSet<Contract> contracts = getSpecificationRepository().getContracts(type, target);
+                    ImmutableSet<Contract> contracts =
+                        getSpecificationRepository().getContracts(type, target);
                     for (Contract contract : contracts) {
                         proofContracts.add(contract);
                     }

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -123,7 +123,7 @@ void selectedBuiltInRule(Goal goal, BuiltInRule rule, PosInOccurrence pos,
      *
      * @param proof The {@link Proof} to start auto mode of.
      */
-    default void startAutoMode(Proof proof) { startAutoMode(proof, proof.openEnabledGoals());}
+    default void startAutoMode(Proof proof) { startAutoMode(proof, proof.openEnabledGoals()); }
 
     /**
      * Starts the auto mode for the given {@link Proof} and the given {@link Goal}s.
@@ -158,7 +158,8 @@ void selectedBuiltInRule(Goal goal, BuiltInRule rule, PosInOccurrence pos,
      * @param proof The {@link Proof} to start auto mode and to wait for.
      * @param goals The {@link Goal}s to close.
      */
-    void startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals) throws InterruptedException;
+    void startAndWaitForAutoMode(Proof proof, ImmutableList<Goal> goals)
+            throws InterruptedException;
 
     /**
      * Starts the auto mode for the given proof which must be contained in this user interface and

key.core/src/main/java/de/uka/ilkd/key/control/ProofControl.java

@@ -18,7 +18,8 @@ public class ProofMacroFacade {
     private static ProofMacroFacade INSTANCE;
 
     public static ProofMacroFacade instance() {
-        if (INSTANCE == null) INSTANCE = new ProofMacroFacade();
+        if (INSTANCE == null)
+            INSTANCE = new ProofMacroFacade();
         return INSTANCE;
     }