From 06995588538a7a41a35eb2f2188986a2755eec07 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 22 May 2015 11:37:45 +0200
Subject: [PATCH] Limit size of VC info in verif report
---
.../scala/leon/verification/VerificationReport.scala | 11 ++++++++++-
1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 0667ed672..ec8342f73 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -23,6 +23,15 @@ case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
lazy val totalInvalid: Int = vrs.count(_._2.isInvalid)
lazy val totalUnknown: Int = vrs.count(_._2.isInconclusive)
+ def sizeLimit(str: String, limit: Int): String = {
+ require(limit > 3)
+ if (str.length > limit) {
+ str.substring(0, limit-3)+"..."
+ } else {
+ str
+ }
+ }
+
def summaryString : String = if(totalConditions >= 0) {
import utils.ASCIIHelpers._
@@ -32,7 +41,7 @@ case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
val timeStr = vr.timeMs.map(t => f"${t/1000d}%-3.3f").getOrElse("")
Row(Seq(
Cell(vc.fd.id.toString),
- Cell(vc.kind.name),
+ Cell(sizeLimit(vc.kind.name, 30)),
Cell(vc.getPos),
Cell(vr.status),
Cell(vr.solvedWith.map(_.name).getOrElse("")),
--
GitLab