Add BlockFailureMessages to report a block level failure immediately

viperproject · Aug 29, 2024 · 395a1a4 · 395a1a4
1 parent b32f732
commit 395a1a4
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 5 deletions.
diff --git 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"
 }
diff --git 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" )