diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index ee185e9..1b6b0bf 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/src/main/scala/viper/server/core/VerificationWorker.scala @@ -154,6 +154,12 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend, val res = for { filteredProgram <- filter(_ast) innerProgram <- beforeVerify(filteredProgram) + stats = StatisticsReport(innerProgram.methods.size, + innerProgram.functions.size, + innerProgram.predicates.size, + innerProgram.domains.size, + innerProgram.fields.size) + _ = _frontend.reporter.report(stats) cachingResult = caching(innerProgram) verificationResult <- verification(cachingResult.transformedProgram) combinedVerificationResult = postCaching(cachingResult, verificationResult) diff --git a/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala b/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala index 9fd48bd..39f4e6f 100644 --- a/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala +++ b/src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala @@ -129,27 +129,9 @@ trait ProgramDefinitionsProvider { } flatten) toList } - private def countInstances(p: Program): Map[String, Int] = p.members.groupBy({ - case _: Method => "method" - case _: Function => "function" - case _: Predicate => "predicate" - case _: Domain => "domain" - case _: Field => "field" - case _ => "other" - }).view.mapValues(_.size).toMap - def reportProgramStats(): Unit = { val prog = _frontend.program.get - val stats = countInstances(prog) - _frontend.reporter.report(ProgramOutlineReport(prog.members.toList)) - _frontend.reporter.report(StatisticsReport( - stats.getOrElse("method", 0), - stats.getOrElse("function", 0), - stats.getOrElse("predicate", 0), - stats.getOrElse("domain", 0), - stats.getOrElse("field", 0) - )) _frontend.reporter.report(ProgramDefinitionsReport(collect(prog))) } } \ No newline at end of file