From a05c87e571eff31bb341703319a6b4ffd93a6d93 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 26 May 2015 14:25:11 +0200
Subject: [PATCH] Fix info being too large in precondition.
---
src/main/scala/leon/verification/DefaultTactic.scala | 2 +-
.../scala/leon/verification/InductionTactic.scala | 2 +-
src/main/scala/leon/verification/Tactic.scala | 12 ++++++++----
.../scala/leon/verification/VerificationReport.scala | 12 +-----------
4 files changed, 11 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index a1cb99a49..3026068a1 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -33,7 +33,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
val vc = implies(and(precOrTrue(fd), path), pre2)
- val fiS = exprToShortString(fi)
+ val fiS = sizeLimit(fi.toString, 40)
VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
}
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 4fc868f9e..bc26e7796 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -78,7 +78,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val vc = implies(and(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd), path), implies(andJoin(subCases), replace((tfd.params.map(_.toVariable) zip args).toMap, pre)))
// Crop the call to display it properly
- val fiS = exprToShortString(fi)
+ val fiS = sizeLimit(fi.toString, 25)
VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fiS, ind. on ($arg : ${cct.classDef.id)}"), this).setPos(fi)
}
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index b424abf5f..b6cb76117 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -31,10 +31,14 @@ abstract class Tactic(vctx: VerificationContext) {
CollectorWithPaths(f).traverse(expr)
}
- protected def exprToShortString(e: Expr) = {
+ protected def sizeLimit(s: String, limit: Int) = {
+ require(limit > 3)
// Crop the call to display it properly
- val eS = e.toString
- val s = eS.takeWhile(_ != '\n').take(35)
- if (s == eS) s else s ++ " ..."
+ val res = s.takeWhile(_ != '\n').take(limit)
+ if (res == s) {
+ res
+ } else {
+ res + " ..."
+ }
}
}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 495ab09f7..0667ed672 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -23,16 +23,6 @@ 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)
- val res = str.takeWhile(_ != '\n').take(35)
- if (res != str) {
- res + "..."
- } else {
- str
- }
- }
-
def summaryString : String = if(totalConditions >= 0) {
import utils.ASCIIHelpers._
@@ -42,7 +32,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(sizeLimit(vc.kind.name, 30)),
+ Cell(vc.kind.name),
Cell(vc.getPos),
Cell(vr.status),
Cell(vr.solvedWith.map(_.name).getOrElse("")),
--
GitLab