From 625426f02f56c20f516f2a9feccd24dc5ec40f3f Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Mon, 4 Dec 2023 10:56:31 +0100
Subject: [PATCH 1/2] tests that gobra messages are printable

---
 src/test/scala/viper/gobra/GobraTests.scala | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
index 057d0fdb8..d5ae82305 100644
--- 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
+    }
+  }
 }

From ea83cd1421c7a5050ae28757180b93d63e771990 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Mon, 4 Dec 2023 13:43:21 +0100
Subject: [PATCH 2/2] fixes unhandled termination measure in pretty printer

---
 src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
index 4a950981e..f7dd0caa5 100644
--- 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)
     }
   }