fixes a unit test

koflin · Mar 10, 2023 · 04874c9 · 04874c9
1 parent a2b9b6c
commit 04874c9
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 6 deletions.
diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala
@@ -24,6 +24,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   def show(node: PNode): Doc = node match {
     case n: PPackage => showPackage(n)
     case n: PProgram => showProgram(n)
+    case n: PPreamble => showPreamble(n)
     case n: PPackageClause => showPackageClause(n)
     case n: PImport => showImport(n)
     case n: PMember => showMember(n)
@@ -61,12 +62,22 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
 
   def showProgram(p: PProgram): Doc = p match {
     case PProgram(packageClause, progPosts, imports, declarations) =>
-      vcat(progPosts.map("initEnsures" <+> showExpr(_))) <>
-        showPackageClause(packageClause) <> line <> line <>
-        ssep(imports map showImport, line) <> line <>
+      showPreamble(packageClause, progPosts, imports) <>
         ssep(declarations map showMember, line <> line) <> line
   }
 
+  // preamble
+
+  def showPreamble(p: PPreamble): Doc = p match {
+    case PPreamble(packageClause, progPosts, imports) =>
+      showPreamble(packageClause, progPosts, imports)
+  }
+
+  private def showPreamble(packageClause: PPackageClause, progPosts: Vector[PExpression], imports: Vector[PImport]): Doc =
+    vcat(progPosts.map("initEnsures" <+> showExpr(_))) <>
+      showPackageClause(packageClause) <> line <> line <>
+      ssep(imports map showImport, line) <> line
+
   // package
 
   def showPackageClause(node: PPackageClause): Doc = "package" <+> showPackageId(node.id)

diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -56,7 +56,7 @@ object Desugar extends LazyLogging {
       // registers main package to generate proof obligations for its init code
       mainDesugarer.registerMainPackage(pkg, importsCollector)(config)
       val res = (mainDesugarer, mainDesugarer.packageD(pkg))
-      logger.debug {
+      logger.trace {
         val durationS = f"${(System.currentTimeMillis() - mainDesugaringStartMs) / 1000f}%.1f"
         s"desugaring package ${info.pkgInfo.id} done, took ${durationS}s"
       }
@@ -68,7 +68,7 @@ object Desugar extends LazyLogging {
     val futResults = Await.result(allPackagesFut, Duration.Inf)
     val (mainDesugarer, mainProgram) = futResults.head
     val importedPrograms = futResults.tail
-    logger.debug {
+    logger.trace {
       val importedDurationS = f"${importeDesugaringDurationMs.get() / 1000f}%.1f"
       s"desugaring imported packages done, took ${importedDurationS}s"
     }

diff --git a/src/test/resources/regressions/features/errors/error-fail2.gobra b/src/test/resources/regressions/features/errors/error-fail2.gobra
@@ -3,7 +3,7 @@
 
 package pkg
 
-// ##(-I src/test/resources/regressions/features/errors)
+// ##(-I ./)
 import . "bar"
 
 func foo(e error) int {