Fixes Issue #781 by converting paths first to absolut paths before re…

…solving their parent path
viperproject · Aug 27, 2024 · 4bf36eb · 4bf36eb
1 parent b28b858
commit 4bf36eb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala
@@ -219,7 +219,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
           inFileConfig <- new ScallopGobraConfig(args, isInputOptional = true, skipIncludeDirChecks = true).config
           resolvedConfig = inFileConfig.copy(includeDirs = inFileConfig.includeDirs.map(
             // it's important to convert includeDir to a string first as `path` might be a ZipPath and `includeDir` might not
-            includeDir => Paths.get(input.name).getParent.resolve(includeDir.toString)))
+            includeDir => Paths.get(input.name).toAbsolutePath.getParent.resolve(includeDir.toString)))
         } yield Some(resolvedConfig)
       }
     })

diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala
@@ -65,7 +65,7 @@ object Source {
      * A unique identifier for packages
      */
     val packageId: String = {
-      val prefix = uniquePath(TransformableSource(src).toPath.getParent, projectRoot).toString
+      val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString
       if(prefix.nonEmpty) {
         // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name
         // per Go's spec (https://go.dev/ref/spec#Package_clause)