spotless

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/IncludeFinder.java

@@ -57,9 +57,10 @@ private void addInclude(String filename) throws MalformedURLException {
         filename = filename.replace('/', File.separatorChar); // Not required for Windows, but
         // whatsoever
         filename = filename.replace('\\', File.separatorChar); // Special handling for Linux
-        var path = base.resolve(filename).normalize();
+        var path = base.resolve(filename).normalize().toAbsolutePath();
 
         var url = path.toUri().toURL();
+        // url = URI.create(path.toString()).toURL();
         source = RuleSourceFactory.initRuleFile(url);
         if (ldt) {
             includes.putLDT(filename, source);

key.core/src/main/java/de/uka/ilkd/key/proof/Node.java

@@ -504,8 +504,8 @@ public int getChildNr(Node child) {
         return -1;
     }
 
-    public StringBuffer getUniqueTacletId() {
-        StringBuffer id = new StringBuffer();
+    public StringBuilder getUniqueTacletId() {
+        StringBuilder id = new StringBuilder(32);
         int c = 0;
         Node n = this;
 

key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java

@@ -5,6 +5,7 @@
 
 import java.util.*;
 import java.util.function.Function;
+import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
 import de.uka.ilkd.key.java.ast.JavaProgramElement;
@@ -265,23 +266,16 @@ public Object clone() {
     }
 
     @Override
-    public @NonNull Set<NoPosTacletApp> allNoPosTacletApps() {
-        Set<NoPosTacletApp> result = new LinkedHashSet<>();
-        for (ImmutableList<NoPosTacletApp> tacletApps : rwList.values()) {
-            tacletApps.forEach(result::add);
-        }
-
-        for (ImmutableList<NoPosTacletApp> tacletApps : antecList.values()) {
-            tacletApps.forEach(result::add);
-        }
-
-        for (ImmutableList<NoPosTacletApp> tacletApps : succList.values()) {
-            tacletApps.forEach(result::add);
-        }
-
-        noFindList.forEach(result::add);
+    public Set<NoPosTacletApp> allNoPosTacletApps() {
+        return allNoPosTacletAppsStream().collect(Collectors.toUnmodifiableSet());
+    }
 
-        return result;
+    public Stream<NoPosTacletApp> allNoPosTacletAppsStream() {
+        Stream<NoPosTacletApp> s1 = rwList.values().stream().flatMap(ImmutableList::stream);
+        Stream<NoPosTacletApp> s2 = antecList.values().stream().flatMap(ImmutableList::stream);
+        Stream<NoPosTacletApp> s3 = succList.values().stream().flatMap(ImmutableList::stream);
+        Stream<NoPosTacletApp> s4 = noFindList.stream();
+        return Stream.concat(Stream.concat(Stream.concat(s1, s2), s3), s4);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

@@ -617,8 +617,8 @@ private InitConfig prepare(EnvInput envInput, InitConfig referenceConfig)
             if (type instanceof ClassDeclaration || type instanceof InterfaceDeclaration) {
                 for (Field f : javaInfo.getAllFields((TypeDeclaration) type)) {
                     final ProgramVariable pv = (ProgramVariable) f.getProgramVariable();
-                        if (pv instanceof LocationVariable lv) {
-                            heapLDT.getFieldSymbolForPV(lv, initConfig.getServices());
+                    if (pv instanceof LocationVariable lv) {
+                        heapLDT.getFieldSymbolForPV(lv, initConfig.getServices());
                     }
                 }
             }

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java

@@ -456,9 +456,25 @@ private TacletApp constructTacletApp(TacletAppIntermediate currInterm, Goal curr
         TacletApp ourApp;
         PosInOccurrence pos = null;
 
-        Taclet t = proof.getInitConfig().lookupActiveTaclet(new Name(tacletName));
+        Name nTacletName = new Name(tacletName);
+        Taclet t = proof.getInitConfig().lookupActiveTaclet(nTacletName);
         if (t == null) {
-            ourApp = currGoal.indexOfTaclets().lookup(tacletName);
+            var possibleApps = currGoal.indexOfTaclets().allNoPosTacletAppsStream()
+                    .filter(it -> it.taclet().name().equals(nTacletName))
+                    .toList();
+
+            if (possibleApps.isEmpty()) {
+                ourApp = null;
+            } else if (possibleApps.size() == 1) {
+                ourApp = possibleApps.getFirst();
+            } else {
+                var taclets = possibleApps.stream().map(TacletApp::toString)
+                        .collect(Collectors.joining("\n---\n"));
+                throw new TacletAppConstructionException(
+                    "There are more than one possible taclet available with name \"" + tacletName
+                        + "\". " +
+                        "Most three similar names are: " + taclets);
+            }
         } else {
             ourApp = NoPosTacletApp.createNoPosTacletApp(t);
         }

key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java

@@ -167,8 +167,9 @@ protected void applyAddrule(ImmutableList<? extends org.key_project.prover.rules
         var matchCond = (MatchConditions) p_matchCond;
         for (var tacletToAdd : rules) {
             final Node n = goal.node();
-            tacletToAdd = tacletToAdd
-                    .setName(tacletToAdd.name() + AUTO_NAME + n.getUniqueTacletId());
+            String name = tacletToAdd.name() + AUTO_NAME + n.getUniqueTacletId();
+            System.out.println(name);
+            tacletToAdd = tacletToAdd.setName(name);
 
 
             // the new Taclet may contain variables with a known

key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java

@@ -8,10 +8,8 @@
 import java.net.URI;
 import java.net.URISyntaxException;
 import java.nio.file.Paths;
-import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
-import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.util.parsing.HasLocation;

key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java

@@ -5,7 +5,6 @@
 
 import java.util.Iterator;
 
-import org.jspecify.annotations.NonNull;
 import org.key_project.logic.ChoiceExpr;
 import org.key_project.logic.Name;
 import org.key_project.logic.SyntaxElement;
@@ -24,6 +23,7 @@
 import org.checkerframework.checker.calledmethods.qual.RequiresCalledMethods;
 import org.checkerframework.checker.initialization.qual.UnderInitialization;
 import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
+import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
 import static org.key_project.util.Strings.formatAsList;

key.ui/src/main/java/de/uka/ilkd/key/core/Log.java

@@ -55,6 +55,9 @@ public static void configureLogging(@Nullable Integer verbosity) {
                 .getLogger(org.slf4j.Logger.ROOT_LOGGER_NAME);
         if (verbosity != null) {
             Appender<ILoggingEvent> consoleAppender = root.getAppender("STDOUT");
+            if (consoleAppender == null) {
+                return;
+            }
             consoleAppender.clearAllFilters();
             var filter = new ThresholdFilter();
             consoleAppender.addFilter(filter);