repair rebase / spotless

wadoon · wadoon · commit 503b69dbf515 · 2025-06-20T13:45:06.000+02:00
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/OutputEnvironment.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/OutputEnvironment.java
@@ -11,6 +11,7 @@
 
 /**
  * This class manages the different paths in the output folder.
+ *
  * @author Alexander Weigl
  * @version 1 (02.02.24)
  */
@@ -37,6 +38,7 @@ public Path getReadmeFile() {
 
     /**
      * Initialize/create the necessary directories.
+     *
      * @throws IOException if the output folder is not write or the folders can not be created.
      */
     public void init() throws IOException {
@@ -47,7 +49,8 @@ public void init() throws IOException {
 
     private void installAntFile() throws IOException {
         try (var buildXml = getClass().getResourceAsStream("/de/uka/ilkd/key/tcg/build.xml")) {
-            Files.copy(Objects.requireNonNull(buildXml), getAntFile(), StandardCopyOption.REPLACE_EXISTING);
+            Files.copy(Objects.requireNonNull(buildXml), getAntFile(),
+                StandardCopyOption.REPLACE_EXISTING);
         }
     }
 }
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
@@ -52,10 +52,12 @@ public IProgramMethod getMUT() {
     @Nullable
     public String getMUTCall() {
         var m = getMUT();
-        if (m == null) return null;
+        if (m == null)
+            return null;
 
         var name = m.getFullName();
-        if (name == null) return null;
+        if (name == null)
+            return null;
 
         StringBuilder params = new StringBuilder();
         for (ParameterDeclaration p : m.getParameters()) {
@@ -93,7 +95,7 @@ public KeYJavaType getTypeOfClassUnderTest() {
 
     @Nullable
     public KeYJavaType getReturnType() {
-        var mut =  getMUT();
+        var mut = getMUT();
         return mut != null ? mut.getType() : null;
     }
 
@@ -119,7 +121,7 @@ public JTerm getPreConTerm() {
         if (c instanceof FunctionalOperationContract t) {
             OriginalVariables orig = t.getOrigVars();
             return t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
-                    orig.params, orig.atPres, services);
+                orig.params, orig.atPres, services);
         }
         // no pre <==> false
         return services.getTermBuilder().ff();
@@ -209,7 +211,7 @@ private String processUpdate(JTerm update) {
                 return "";
             }
             return "   \n" + up.lhs().sort() + " " + up.lhs().toString() + " = " + update.sub(0)
-                    + ";";
+                + ";";
         }
         StringBuilder result = new StringBuilder();
         for (JTerm sub : update.subs()) {
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
@@ -41,7 +41,6 @@
 import org.jspecify.annotations.Nullable;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.sort.Sort;
-import org.key_project.logic.sort.Sort;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.java.StringUtil;
 
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java
@@ -10,7 +10,6 @@
 
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.prover.ProverTaskListener;
 import de.uka.ilkd.key.settings.DefaultSMTSettings;
 import de.uka.ilkd.key.settings.NewSMTTranslationSettings;
 import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
@@ -25,33 +24,29 @@
 import de.uka.ilkd.key.testgen.smt.testgen.TGPhase;
 import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLifecycleListener;
 
+import org.key_project.prover.engine.ProverTaskListener;
+
 public record TestgenFacade(TestGenerationSettings settings) {
     public static Callable<Boolean> generateTestcasesTask(KeYEnvironment<?> env, Proof proof,
-                                                          TestGenerationSettings settings,
-                                                          TestGenerationLifecycleListener log) {
+            TestGenerationSettings settings,
+            TestGenerationLifecycleListener log) {
         return () -> {
             generateTestcases(env, proof, settings, log);
             return true;
         };
     }
 
-    /**
-     * @param env
-     * @param proof
-     * @param settings
-     * @param log
-     * @throws InterruptedException
-     */
     public static void generateTestcases(KeYEnvironment<?> env, Proof proof,
-                                         TestGenerationSettings settings,
-                                         TestGenerationLifecycleListener log) throws InterruptedException {
+            TestGenerationSettings settings,
+            TestGenerationLifecycleListener log) throws InterruptedException {
         final TGReporter reporter = new TGReporter(log);
 
         final TestCaseGenerator tg = new TestCaseGenerator(proof, settings, reporter);
 
         NewSMTTranslationSettings newSettings = new NewSMTTranslationSettings();
         ProofDependentSMTSettings pdSettings = ProofDependentSMTSettings.getDefaultSettingsData();
-        ProofIndependentSMTSettings piSettings = ProofIndependentSMTSettings.getDefaultSettingsData();
+        ProofIndependentSMTSettings piSettings =
+            ProofIndependentSMTSettings.getDefaultSettingsData();
 
         piSettings.setTimeout(10000);
         final var smtSettings = new DefaultSMTSettings(pdSettings, piSettings, newSettings, proof);
@@ -60,7 +55,7 @@ public static void generateTestcases(KeYEnvironment<?> env, Proof proof,
         launcher.addListener(new SolverLauncherListener() {
             @Override
             public void launcherStopped(SolverLauncher launcher,
-                                        Collection<SMTSolver> finishedSolvers) {
+                    Collection<SMTSolver> finishedSolvers) {
                 try {
                     var first = finishedSolvers.iterator().next();
                     if (first.getException() != null) {
@@ -80,7 +75,7 @@ public void launcherStopped(SolverLauncher launcher,
 
             @Override
             public void launcherStarted(Collection<SMTProblem> problems,
-                                        Collection<SolverType> solverTypes, SolverLauncher launcher) {
+                    Collection<SolverType> solverTypes, SolverLauncher launcher) {
             }
         });
 
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java
@@ -6,6 +6,7 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.macros.AbstractBlastingMacro;
+
 import org.key_project.prover.proof.rulefilter.RuleFilter;
 import org.key_project.prover.rules.Rule;
 
@@ -126,8 +127,9 @@ public String getDescription() {
 
     private record NameRuleFilter(Set<String> rules) implements RuleFilter {
 
-    @Override
-    public boolean filter(Rule rule) {
-        return rules.contains(rule.name().toString());
+        @Override
+        public boolean filter(Rule rule) {
+            return rules.contains(rule.name().toString());
+        }
     }
-}}
+}
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java
@@ -5,20 +5,13 @@
 
 import java.util.Set;
 
-import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.macros.FilterStrategy;
 import de.uka.ilkd.key.macros.ModalityCache;
 import de.uka.ilkd.key.macros.StrategyProofMacro;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.rule.Rule;
-import de.uka.ilkd.key.rule.RuleApp;
-import de.uka.ilkd.key.strategy.NumberRuleAppCost;
-import de.uka.ilkd.key.strategy.RuleAppCost;
-import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
 import de.uka.ilkd.key.strategy.Strategy;
-import de.uka.ilkd.key.strategy.feature.MutableState;
 import de.uka.ilkd.key.testgen.TestGenerationSettings;
 
 import org.key_project.logic.Name;
@@ -31,7 +24,6 @@
 import org.key_project.prover.strategy.costbased.RuleAppCost;
 
 import org.jspecify.annotations.NonNull;
-
 import org.jspecify.annotations.Nullable;
 
 public class TestGenMacro extends StrategyProofMacro {
@@ -74,17 +66,8 @@ class TestGenStrategy extends FilterStrategy {
      * the modality cache used by this strategy
      */
     private final ModalityCache modalityCache = new ModalityCache();
-    static {
-        unwindRules = new HashSet<>();
-        unwindRules.add("loopUnwind");
-        unwindRules.add("doWhileUnwind");
-        unwindRules.add("methodCall");
-        unwindRules.add("methodCallWithAssignment");
-        unwindRules.add("staticMethodCall");
-        unwindRules.add("staticMethodCallWithAssignment");
-    }
 
-    private static boolean isUnwindRule(@Nullable Rule rule) {
+    private static boolean isUnwindRule(org.key_project.prover.rules.Rule rule) {
         if (rule == null) {
             return false;
         }
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java
@@ -6,16 +6,14 @@
 import java.util.*;
 
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.ldt.JavaDLTheory;
 import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.sort.SortImpl;
 import de.uka.ilkd.key.smt.NumberTranslation;
 import de.uka.ilkd.key.testgen.ReflectionClassCreator;
 import de.uka.ilkd.key.testgen.oracle.OracleUnaryTerm.Op;
 
-import org.key_project.logic.Name;
-import org.key_project.logic.op.Function;
-import org.key_project.logic.sort.Sort;
 import org.key_project.logic.Name;
 import org.key_project.logic.Term;
 import org.key_project.logic.op.Function;
@@ -27,7 +25,6 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import static de.uka.ilkd.key.ldt.JavaDLTheory.FORMULA;
 import static de.uka.ilkd.key.testgen.Constants.*;
 
 public class OracleGenerator {
@@ -52,6 +49,7 @@ public class OracleGenerator {
     private Set<String> truePredicates = new TreeSet<>();
 
     private Set<String> falsePredicates = new TreeSet<>();
+
     private final Set<String> prestateTerms = new TreeSet<>();
 
     private final Map<Sort, OracleMethod> invariants = new HashMap<>();
@@ -467,7 +465,7 @@ private OracleTerm translateSelect(Term term, boolean initialSelect) {
 
         if (!initialSelect && isPreHeap(heapTerm)
                 && term.sort().extendsTrans(services.getJavaInfo().getJavaLangObject().getSort())) {
-            return new OracleConstant(TestCaseGenerator.OLDMap + ".get(" + value + ")",
+            return new OracleConstant(OLD_MAP + ".get(" + value + ")",
                 term.sort());
         }
 
@@ -589,9 +587,9 @@ private OracleMethod createIfThenElseMethod(Term term, boolean initialSelect) {
     private String getSetName(Sort s) {
 
         if (s.equals(JavaDLTheory.FORMULA)) {
-            return TestCaseGenerator.ALL_BOOLS;
+            return ALL_BOOLS;
         } else if (s.equals(services.getTypeConverter().getIntegerLDT().targetSort())) {
-            return TestCaseGenerator.ALL_INTS;
+            return ALL_INTS;
         } else if (s.equals(services.getTypeConverter().getLocSetLDT().targetSort())) {
             throw new RuntimeException("Not implemented yet.");
             // return TestCaseGenerator.ALL_LOCSETS
@@ -607,7 +605,7 @@ private String getSetName(Sort s) {
         }
 
 
-        return TestCaseGenerator.ALL_OBJECTS;
+        return ALL_OBJECTS;
     }
 
     private OracleMethod createQuantifierMethod(Term term, boolean initialSelect) {
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocationSet.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocationSet.java
@@ -9,8 +9,7 @@
 public sealed
 
 interface OracleLocationSet
-permits AllLocsLocationSet, EmptyOracleLocationSet, OracleDefaultLocationSet
-{
+        permits AllLocsLocationSet, EmptyOracleLocationSet, OracleDefaultLocationSet {
 
     static OracleLocationSet singleton(OracleLocation loc) {
         var result = new OracleDefaultLocationSet();
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethodCall.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethodCall.java
@@ -9,7 +9,7 @@
 import org.jspecify.annotations.Nullable;
 
 public record OracleMethodCall(OracleMethod method, List<? extends OracleTerm> args,
-                               @Nullable OracleTerm caller)
+        @Nullable OracleTerm caller)
         implements OracleTerm {
     public OracleMethodCall(OracleMethod method, List<? extends OracleTerm> args) {
         this(method, args, null);
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleTerm.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleTerm.java
@@ -3,8 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.testgen.oracle;
 
-public sealed
-interface OracleTerm
-permits OracleBinTerm, OracleConstant, OracleMethodCall, OracleType, OracleUnaryTerm, OracleVariable
-{
+public sealed interface OracleTerm
+        permits OracleBinTerm, OracleConstant, OracleMethodCall, OracleType, OracleUnaryTerm,
+        OracleVariable {
 }
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java
@@ -7,6 +7,7 @@
 
 public record OracleVariable(String name, Sort sort) implements OracleTerm {
     public String toString() {
-        return name;}
+        return name;
+    }
 
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java
@@ -46,7 +46,6 @@
 import org.key_project.prover.strategy.costbased.TopRuleAppCost;
 import org.key_project.util.collection.ImmutableList;
 
-
 import org.jspecify.annotations.NonNull;
 
 public abstract class AbstractBlastingMacro extends StrategyProofMacro {
diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java
@@ -17,8 +17,6 @@
 import de.uka.ilkd.key.gui.actions.MainWindowAction;
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.smt.SolverListener;
-import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro;
 import de.uka.ilkd.key.proof.*;
 import de.uka.ilkd.key.settings.DefaultSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
@@ -147,9 +145,6 @@ private boolean checkZ3CE() {
      */
     public static class NoMainWindowCounterExampleGenerator
             extends AbstractSideProofCounterExampleGenerator {
-        /**
-         * {@inheritDoc}
-         */
         @Override
         protected SolverLauncherListener createSolverListener(DefaultSMTSettings settings,
                 Proof proof) {
