Add block level message types

.gitignore

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

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

@@ -326,3 +326,24 @@ case class VerificationTerminationMessage() extends Message {
   override val toString: String = "verification_termination_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"
+}
+
+/** 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, 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"
+}

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

@@ -75,6 +75,9 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
       case q: QuantifierInstantiationsMessage => csv_file.write(s"${q.toString}\n")
       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 f: BlockFailureMessage => csv_file.write(s"${f.toString}\n")
+      case p: PathProcessedMessage => csv_file.write(s"${p.toString}\n")
       case _ =>
         println( s"Cannot properly print message of unsupported type: $msg" )
     }
@@ -188,6 +191,9 @@ 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 _: BlockFailureMessage =>  // println(msg)
+      case _: PathProcessedMessage =>  // println(msg)
       case _ =>
         println( s"Cannot properly print message of unsupported type: $msg" )
     }