From 53078306a0bb028b1e66290ff34767b8e1fdfa11 Mon Sep 17 00:00:00 2001
From: jad <you@example.com>
Date: Mon, 2 May 2016 14:09:20 +0200
Subject: [PATCH] added pretty printing for termination checker
---
src/main/scala/leon/termination/TerminationPhase.scala | 2 +-
src/main/scala/leon/termination/TerminationReport.scala | 9 +++++++--
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index d5b07f276..a7802c490 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -30,6 +30,6 @@ object TerminationPhase extends SimpleLeonPhase[Program, TerminationReport] {
}
val endTime = System.currentTimeMillis
- new TerminationReport(ctx, results, (endTime - startTime).toDouble / 1000.0d)
+ new TerminationReport(ctx, tc.program, results, (endTime - startTime).toDouble / 1000.0d)
}
}
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index c7fc3a0b3..47ef92268 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -6,8 +6,10 @@ package termination
import purescala.Definitions._
import utils.Report
import utils.ASCIIHelpers._
+import leon.purescala.PrettyPrinter
+import leon.purescala.SelfPrettyPrinter
-case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
+case class TerminationReport(ctx: LeonContext, program: Program, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
def summaryString : String = {
var t = Table("Termination summary")
@@ -18,7 +20,10 @@ case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,Termination
val result = if (g.isGuaranteed) "\u2713" else "\u2717"
val verdict = g match {
case LoopsGivenInputs(reason, args) =>
- "Non-terminating for call: " + args.mkString(fd.id + "(", ",", ")")
+ val niceArgs = args.map { v =>
+ SelfPrettyPrinter.print(v, PrettyPrinter(v))(ctx, program)
+ }
+ "Non-terminating for call: " + niceArgs.mkString(fd.id + "(", ",", ")")
case CallsNonTerminating(funDefs) =>
"Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
case Terminates(reason) =>
--
GitLab