tests that gobra messages are printable

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
+    }
+  }
 }