fix Windows relative root problem

Author: wadoon

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

@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.pp.LogicPrinter;
 import de.uka.ilkd.key.pp.NotationInfo;
 import de.uka.ilkd.key.pp.PrettyPrinter;
+import de.uka.ilkd.key.proof.JavaModel;
 import de.uka.ilkd.key.proof.NameRecorder;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
@@ -40,8 +41,8 @@
 import de.uka.ilkd.key.smt.SMTRuleApp;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.util.KeYConstants;
-import de.uka.ilkd.key.util.MiscTools;
 
+import org.jspecify.annotations.NonNull;
 import org.key_project.logic.Name;
 import org.key_project.logic.PosInTerm;
 import org.key_project.logic.op.Modality;
@@ -56,7 +57,7 @@
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.java.IOUtil;
+import org.key_project.util.collection.ImmutableMapEntry;
 
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
@@ -144,7 +145,7 @@ public String writeSettings(ProofSettings ps) {
 
     public void save(Path basePath, OutputStream out) throws IOException {
         CopyReferenceResolver.copyCachedGoals(proof, null, null, null);
-        try (var ps = new PrintWriter(out, true, StandardCharsets.UTF_8)) {
+        try (PrintWriter ps = new PrintWriter(out, true, StandardCharsets.UTF_8)) {
             final ProofOblInput po =
                 proof.getServices().getSpecificationRepository().getProofOblInput(proof);
             LogicPrinter printer = createLogicPrinter(proof.getServices(), false);
@@ -167,14 +168,14 @@ public void save(Path basePath, OutputStream out) throws IOException {
             ps.println(writeSettings(proof.getSettings()));
 
 
-            var header = proof.header();
+            KeyAst.Declarations header = proof.header();
             String headerStr = makePathsRelative(basePath, header);
             ps.print(headerStr);
 
             proof.printSymbols(ps);
 
             // \problem or \proofObligation
-            var hasProofObligation =
+            boolean hasProofObligation =
                 po instanceof IPersistablePO ppo && ppo.printProofObligation(ps, proof);
 
 
@@ -218,10 +219,9 @@ public void save(Path basePath, OutputStream out) throws IOException {
     /// Better would be to get rid of the header, and using an AST.
     ///
     ///
-    /// @see KeYUserProblemFile#getProblemHeader()
+    /// @see de.uka.ilkd.key.proof.init.KeYUserProblemFile#getProblemHeader()
     /// @see de.uka.ilkd.key.proof.init.InitConfig#getProblemHeader()
-    private String makePathsRelative(Path basePath, KeyAst.@Nullable Declarations header)
-            throws IOException {
+    private String makePathsRelative(Path basePath, KeyAst.@Nullable Declarations header) {
         if (header == null) {
             return "";
         }
@@ -230,28 +230,28 @@ private String makePathsRelative(Path basePath, KeyAst.@Nullable Declarations he
 
         header.printDefinitions(out);
 
-        var jm = proof.getServices().getJavaModel();
+        JavaModel jm = proof.getServices().getJavaModel();
 
-        var bootClassPath = jm.getBootClassPath();
+        Path bootClassPath = jm.getBootClassPath();
         if (bootClassPath != null) {
-            out.printf("\\bootclasspath \"%s\";\n", IOUtil.safePath(bootClassPath));
+            out.printf("\\bootclasspath \"%s\";\n", safePathRelativeTo(bootClassPath, basePath));
         }
 
-        var classPath = jm.getClassPath();
+        List<Path> classPath = jm.getClassPath();
         if (classPath != null && !classPath.isEmpty()) {
             for (Path path : classPath) {
                 out.printf("\\classpath \"%s\";\n", safePathRelativeTo(path, basePath));
             }
         }
 
-        var javaSource = jm.getModelDir();
+        Path javaSource = jm.getModelDir();
         if (javaSource != null) {
             out.printf("\\javaSource \"%s\";\n", safePathRelativeTo(javaSource, basePath));
         }
 
-        var includedFiles = jm.getIncludedFiles();
+        List<Path> includedFiles = jm.getIncludedFiles();
         if (includedFiles != null && !includedFiles.isEmpty()) {
-            for (var includedFile : includedFiles) {
+            for (Path includedFile : includedFiles) {
                 out.printf("\\include \"%s\";\n",
                     safePathRelativeTo(includedFile, basePath));
             }
@@ -260,18 +260,6 @@ private String makePathsRelative(Path basePath, KeyAst.@Nullable Declarations he
         return sw.toString();
     }
 
-    /**
-     * Try to create a relative path, but return the absolute path if a relative path cannot be
-     * found. This may happen on Windows systems (bug #1480).
-     */
-    private static String tryToMakeFilenameRelative(String absPath, String basePath) {
-        try {
-            return MiscTools.makeFilenameRelative(absPath, basePath);
-        } catch (final RuntimeException e) {
-            return absPath;
-        }
-    }
-
     private String newNames2Proof(Node n) {
         StringBuilder s = new StringBuilder();
         final NameRecorder rec = n.getNameRecorder();
@@ -369,9 +357,9 @@ private void printLatticeAbstractionForSingleMergeRuleApp(
             output.append(" (").append(ProofElementID.MERGE_USER_CHOICES.getRawName())
                     .append(" \"");
             boolean first = true;
-            for (var pair : userChoices.entrySet()) {
-                final var key = pair.getKey();
-                final var value = pair.getValue();
+            for (Map.Entry<ProgramVariable, AbstractDomainElement> pair : userChoices.entrySet()) {
+                final ProgramVariable key = pair.getKey();
+                final AbstractDomainElement value = pair.getValue();
                 if (first) {
                     first = false;
                 } else {
@@ -690,7 +678,7 @@ public static String posInTerm2Proof(PosInTerm pos) {
     public Collection<String> getInterestingInstantiations(SVInstantiations inst) {
         Collection<String> s = new ArrayList<>();
 
-        for (final var pair : inst.interesting()) {
+        for (final ImmutableMapEntry<@NonNull SchemaVariable, @NonNull InstantiationEntry<?>> pair : inst.interesting()) {
             final SchemaVariable var = pair.key();
 
             final Object value = pair.value().getInstantiation();

key.util/src/main/java/org/key_project/util/java/IOUtil.java

@@ -831,7 +831,13 @@ public static String safePath(Path path) {
     /// @param basePath a directory
     /// @return a string that is printable (escaped) for KeY files
     public static String safePathRelativeTo(Path source, Path basePath) {
-        var abs = source.toAbsolutePath();
-        return safePath(basePath.relativize(abs));
+        if (Objects.equals(source.getRoot(), basePath.getRoot())) {
+            // required on Windows
+            var abs = source.toAbsolutePath();
+            return safePath(basePath.relativize(abs));
+        } else {
+            // fallback: return absolute path
+            return safePath(source.toAbsolutePath());
+        }
     }
 }