Merge pull request #711 from viperproject/test-gobra-messages

Fixes Pretty Printer
viperproject · Dec 5, 2023 · 4dc33c6 · 4dc33c6
2 parents 9f38d64 + ea83cd1
commit 4dc33c6
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 6 deletions.
diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
@@ -140,10 +140,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     measure match {
       case WildcardMeasure(cond) => "_" <+> showCond(cond)
       case TupleTerminationMeasure(tuple, cond) =>
-        hcat(tuple map {
-          case e: Expr => showExpr(e)
-          case n => violation(s"Unexpected node $n")
-        }) <+> showCond(cond)
+        hcat(tuple map show) <+> showCond(cond)
     }
   }
 

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
@@ -16,7 +16,7 @@ import viper.gobra.frontend.Source.FromFileSource
 import viper.gobra.frontend.info.Info
 import viper.gobra.frontend.{Config, PackageResolver, Parser, Source}
 import viper.gobra.reporting.VerifierResult.{Failure, Success}
-import viper.gobra.reporting.{NoopReporter, VerifierError}
+import viper.gobra.reporting.{GobraMessage, GobraReporter, VerifierError}
 import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, SystemUnderTest}
 import viper.silver.utility.TimingUtils
 import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
@@ -51,7 +51,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
   private def getConfig(source: Source): Config =
     Config(
       logLevel = Level.INFO,
-      reporter = NoopReporter,
+      reporter = StringifyReporter,
       packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)),
       checkConsistency = true,
       cacheParserAndTypeChecker = cacheParserAndTypeChecker,
@@ -120,4 +120,13 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
     /** A short and unique identifier for this output. */
     override def fullId: String = error.id
   }
+
+  case object StringifyReporter extends GobraReporter {
+    override val name: String = "StringifyReporter"
+
+    override def report(msg: GobraMessage): Unit = {
+      // by invoking `toString`, we check that messages are printable, which includes pretty-printing AST nodes:
+      msg.toString
+    }
+  }
 }