Rename BlockProcessedMessage to PathProcessedMessage

Author: trktby

.gitignore

@@ -1,3 +1,4 @@
+.vscode
 .cache
 project/project/**
 bin/**

src/main/scala/viper/silver/reporter/Message.scala

@@ -327,11 +327,15 @@ case class VerificationTerminationMessage() extends Message {
   override val name: String = "verification_termination_message"
 }
 
+/** Reported when a block of a method CFG is reached.
+  */
 case class BlockReachedMessage(methodName: String, label: String, pathId: Int) extends  Message {
   override val toString: String = s"block_reached_message(methodName=$methodName, label=$label, pathId=$pathId)"
   override val name: String = "block_reached_message"
 }
-case class BlockProcessedMessage(methodName: String, label: String, pathId: Int, verificationResult: String) extends  Message {
-  override val toString: String = s"block_processed_message(methodName=$methodName, label=$label, pathId=$pathId, result=\"${if (verificationResult.toString() == "Success") "Success" else "Failure"}\")"
-  override val name: String = "block_processed_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"
 }

src/main/scala/viper/silver/reporter/Reporter.scala

@@ -76,7 +76,7 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
       case q: QuantifierChosenTriggersMessage => csv_file.write(s"${q.toString}\n")
       case t: VerificationTerminationMessage => csv_file.write(s"${t.toString}\n")
       case r: BlockReachedMessage => csv_file.write(s"${r.toString}\n")
-      case p: BlockProcessedMessage => csv_file.write(s"${p.toString}\n")
+      case p: PathProcessedMessage => csv_file.write(s"${p.toString}\n")
       case _ =>
         println( s"Cannot properly print message of unsupported type: $msg" )
     }
@@ -190,8 +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 _: BlockProcessedMessage =>  //println(msg)
+      case _: BlockReachedMessage =>  // println(msg)
+      case _: PathProcessedMessage =>  // println(msg)
       case _ =>
         println( s"Cannot properly print message of unsupported type: $msg" )
     }