From 395a1a44ebcb5ed72f1687f518b2b789f826f3b1 Mon Sep 17 00:00:00 2001
From: trk <trktby@gmail.com>
Date: Thu, 29 Aug 2024 11:33:50 +0200
Subject: [PATCH] Add BlockFailureMessages to report a block level failure
 immediately

---
 .../scala/viper/silver/reporter/Message.scala     | 15 +++++++++++----
 .../scala/viper/silver/reporter/Reporter.scala    |  3 ++-
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/viper/silver/reporter/Message.scala b/src/main/scala/viper/silver/reporter/Message.scala
index 5a0b5dfc7..31b423ca7 100644
--- a/src/main/scala/viper/silver/reporter/Message.scala
+++ b/src/main/scala/viper/silver/reporter/Message.scala
@@ -333,9 +333,16 @@ case class BlockReachedMessage(methodName: String, label: String, pathId: Int) e
   override val toString: String = s"block_reached_message(methodName=$methodName, label=$label, pathId=$pathId)"
   override val name: String = "block_reached_message"
 }
+
+/** Reported when a block of a method CFG failed 
+*/
+case class BlockFailureMessage(methodName: String, label: String, pathId: Int) extends  Message {
+  override val toString: String = s"block_failure_message(methodName=$methodName, label=$label, pathId=$pathId)"
+  override val name: String = "block_failure_message"
+}
 /** Reported when an execution path through a method has completed.
-  */
-case class PathProcessedMessage(methodName: String, label: String, pathId: Int, verificationResultKind: String) extends  Message {
-  override val toString: String = s"Path_processed_message(methodName=$methodName, label=$label, pathId=$pathId, result=$verificationResultKind)"
-  override val name: String = "Path_processed_message"
+*/
+case class PathProcessedMessage(methodName: String, pathId: Int, result: String) extends  Message {
+  override val toString: String = s"path_processed_message(methodName=$methodName, pathId=$pathId, result=$result)"
+  override val name: String = "path_processed_message"
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala
index f8b4ef3c2..496d6748d 100644
--- a/src/main/scala/viper/silver/reporter/Reporter.scala
+++ b/src/main/scala/viper/silver/reporter/Reporter.scala
@@ -190,7 +190,8 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
       case _: QuantifierInstantiationsMessage => // too verbose, do not print
       case _: QuantifierChosenTriggersMessage => // too verbose, do not print
       case _: VerificationTerminationMessage =>
-      case _: BlockReachedMessage =>  // println(msg)
+      case _: BlockReachedMessage => // println(msg)
+      case _: BlockFailureMessage =>  // println(msg)
       case _: PathProcessedMessage =>  // println(msg)
       case _ =>
         println( s"Cannot properly print message of unsupported type: $msg" )