Add logging message with the member name when verification throws an exception

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -223,8 +223,15 @@ class DefaultMainVerifier(config: Config,
      */
     val functionVerificationResults = functionsSupporter.units.toList flatMap (function => {
       val startTime = System.currentTimeMillis()
-      val results = functionsSupporter.verify(createInitialState(function, program, functionData, predicateData), function)
-        .flatMap(extractAllVerificationResults)
+      var results: Seq[VerificationResult] = null
+      try {
+        results = functionsSupporter.verify(createInitialState(function, program, functionData, predicateData), function)
+          .flatMap(extractAllVerificationResults)
+      } catch {
+        case e : Throwable =>
+          logger error s"An exception was thrown while verifying function `${function.name}`."
+          throw e
+      }
       val elapsed = System.currentTimeMillis() - startTime
       reporter report VerificationResultMessage(s"silicon", function, elapsed, condenseToViperResult(results))
       logger debug s"Silicon finished verification of function `${function.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}"
@@ -233,8 +240,15 @@ class DefaultMainVerifier(config: Config,
 
     val predicateVerificationResults = predicateSupporter.units.toList flatMap (predicate => {
       val startTime = System.currentTimeMillis()
-      val results = predicateSupporter.verify(createInitialState(predicate, program, functionData, predicateData), predicate)
-        .flatMap(extractAllVerificationResults)
+      var results: Seq[VerificationResult] = null
+      try {
+        results = predicateSupporter.verify(createInitialState(predicate, program, functionData, predicateData), predicate)
+          .flatMap(extractAllVerificationResults)
+      } catch {
+        case e: Throwable =>
+          logger error s"An exception was thrown while verifying predicate `${predicate.name}`."
+          throw e
+      }
       val elapsed = System.currentTimeMillis() - startTime
       reporter report VerificationResultMessage(s"silicon", predicate, elapsed, condenseToViperResult(results))
       logger debug s"Silicon finished verification of predicate `${predicate.name}` in ${viper.silver.reporter.format.formatMillisReadably(elapsed)} seconds with the following result: ${condenseToViperResult(results).toString}"
@@ -256,14 +270,20 @@ class DefaultMainVerifier(config: Config,
 
     val verificationTaskFutures: Seq[Future[Seq[VerificationResult]]] =
       program.methods.filterNot(excludeMethod).map(method => {
-
         val s = createInitialState(method, program, functionData, predicateData).copy(parallelizeBranches =
           Verifier.config.parallelizeBranches()) /* [BRANCH-PARALLELISATION] */
 
         _verificationPoolManager.queueVerificationTask(v => {
           val startTime = System.currentTimeMillis()
-          val results = v.methodSupporter.verify(s, method)
-            .flatMap(extractAllVerificationResults)
+          var results: Seq[VerificationResult] = null
+          try {
+            results = v.methodSupporter.verify(s, method)
+              .flatMap(extractAllVerificationResults)
+          } catch {
+            case e: Throwable =>
+              logger error s"An exception was thrown while verifying method `${method.name}`."
+              throw e
+          }
           val elapsed = System.currentTimeMillis() - startTime
 
           reporter report VerificationResultMessage(s"silicon", method, elapsed, condenseToViperResult(results))
@@ -276,8 +296,16 @@ class DefaultMainVerifier(config: Config,
 
         _verificationPoolManager.queueVerificationTask(v => {
           val startTime = System.currentTimeMillis()
-          val results = v.cfgSupporter.verify(s, cfg)
-            .flatMap(extractAllVerificationResults)
+
+          var results: Seq[VerificationResult] = null
+          try {
+            results = v.cfgSupporter.verify(s, cfg)
+              .flatMap(extractAllVerificationResults)
+          } catch {
+            case e: Throwable =>
+              logger error s"An exception was thrown while verifying a cfg."
+              throw e
+          }
           val elapsed = System.currentTimeMillis() - startTime
 
           reporter report VerificationResultMessage(s"silicon"/*, cfg*/, elapsed, condenseToViperResult(results))