Add command line option to report partial results via StdIOReporter (#887)

Author: marcoeilers

src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala

@@ -152,6 +152,12 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     noshort = true
   )
 
+  val reportPartialResults = opt[Boolean](name = "reportPartialResults",
+    descr = "Whether to report partial verification success and failure for individual members and branches via the StdIOReporter.",
+    default = Some(false),
+    noshort = true
+  )
+
   validateOpt(file, ignoreFile) {
     case (_, Some(true)) => Right(())
     case (Some(filepath), _) => validateFileOpt(file.name, filepath)

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -233,6 +233,10 @@ trait SilFrontend extends DefaultFrontend {
 
     if (_config != null) {
       resetPlugins()
+      reporter match {
+        case cf: ConfigurableReporter => cf.setConfig(Some(_config))
+        case _ =>
+      }
     }
   }
 

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

@@ -6,6 +6,7 @@
 
 package viper.silver.reporter
 
+import viper.silver.frontend.SilFrontendConfig
 import viper.silver.plugin.SilverPluginManager
 import viper.silver.verifier.Success
 
@@ -23,6 +24,14 @@ object NoopReporter extends Reporter {
   def report(msg: Message): Unit = ()
 }
 
+trait ConfigurableReporter extends Reporter {
+  protected var config: Option[SilFrontendConfig] = None
+
+  def setConfig(c: Option[SilFrontendConfig]): Unit = {
+    config = c
+  }
+}
+
 trait PluginAwareReporter extends Reporter {
 
   protected var plugins: Option[SilverPluginManager] = None
@@ -115,7 +124,8 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv
   }
 }
 
-case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = true) extends PluginAwareReporter {
+case class StdIOReporter(name: String = "stdout_reporter",
+                         timeInfo: Boolean = true) extends PluginAwareReporter with ConfigurableReporter {
 
   var counter = 0
 
@@ -126,6 +136,8 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
 
   private def bulletFmt(num_items: Int): String = s"%${num_items.toString.length}d"
 
+  private def shouldReportPartial = config.isDefined && config.get.reportPartialResults.getOrElse(false)
+
   def doReport(msg: Message): Unit = {
     msg match {
       case AstConstructionFailureMessage(t, res) =>
@@ -209,9 +221,12 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t
         println( s"encountered missing dependency: $text" )
 
       // These get reported without being transformed by any plugins, it would be an issue if we printed them to STDOUT.
-      case EntitySuccessMessage(_, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
-      case EntityFailureMessage(_, _, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
-      case BranchFailureMessage(_, _, _, _) =>    // FIXME Currently, we only print overall verification results to STDOUT.
+      case EntitySuccessMessage(_, _, _, _) =>
+        if (shouldReportPartial) println(msg)
+      case EntityFailureMessage(_, _, _, _, _) =>
+        if (shouldReportPartial) println(msg)
+      case BranchFailureMessage(_, _, _, _) =>
+        if (shouldReportPartial) println(msg)
       case ConfigurationConfirmation(_) =>     // TODO  use for progress reporting
         //println( s"Configuration confirmation: $text" )
       case InternalWarningMessage(_) =>        // TODO  use for progress reporting