From 019b1fad0e5d57fa5a239f5502445fdae2aebde2 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 12 Jul 2010 12:45:59 +0000
Subject: [PATCH] one less bug
---
src/purescala/Analysis.scala | 30 ++++++++++++++++--------------
testcases/MergeSort.scala | 6 ++++--
2 files changed, 20 insertions(+), 16 deletions(-)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 8e7279cd7..e7f958345 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -111,21 +111,23 @@ class Analysis(val program: Program) {
}
}
- verifiedVCs = verifiedVCs.reverse
- val col1wdth = verifiedVCs.map(_._1).map(_.length).max + 2
- val col2wdth = verifiedVCs.map(_._2).map(_.length).max + 2
- val col3wdth = verifiedVCs.map(_._3).map(_.length).max + 2
- val col4wdth = verifiedVCs.map(_._4).map(_.length).max
- def mk1line(line: (String,String,String,String)) : String = {
- line._1 + (" " * (col1wdth - line._1.length)) +
- line._2 + (" " * (col2wdth - line._2.length)) +
- line._3 + (" " * (col3wdth - line._3.length)) +
- line._4
+ if(verifiedVCs.size > 0) {
+ verifiedVCs = verifiedVCs.reverse
+ val col1wdth = verifiedVCs.map(_._1).map(_.length).max + 2
+ val col2wdth = verifiedVCs.map(_._2).map(_.length).max + 2
+ val col3wdth = verifiedVCs.map(_._3).map(_.length).max + 2
+ val col4wdth = verifiedVCs.map(_._4).map(_.length).max
+ def mk1line(line: (String,String,String,String)) : String = {
+ line._1 + (" " * (col1wdth - line._1.length)) +
+ line._2 + (" " * (col2wdth - line._2.length)) +
+ line._3 + (" " * (col3wdth - line._3.length)) +
+ line._4
+ }
+ val dashes : String = "=" * (col1wdth + col2wdth + col3wdth + col4wdth)
+ reporter.info("Summary:\n" + dashes + "\n" + verifiedVCs.map(mk1line(_)).mkString("\n") + "\n" + dashes)
+ } else {
+ reporter.info("No verification conditions were generated.")
}
- val dashes : String = "=" * (col1wdth + col2wdth + col3wdth + col4wdth)
-
- reporter.info("Summary:\n" + dashes + "\n" + verifiedVCs.map(mk1line(_)).mkString("\n") + "\n" + dashes)
-
}
def postconditionVC(functionDefinition: FunDef) : Expr = {
diff --git a/testcases/MergeSort.scala b/testcases/MergeSort.scala
index 565359a77..4dd8a2793 100644
--- a/testcases/MergeSort.scala
+++ b/testcases/MergeSort.scala
@@ -14,8 +14,10 @@ object MergeSort {
def is_sorted(l: List): Boolean = l match {
case Nil() => true
- case Cons(x,Nil()) => true
- case Cons(x,Cons(y,xs)) => x<=y && is_sorted(Cons(y,xs))
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && is_sorted(Cons(y, ys))
+ }
}
def length(list:List): Int = list match {
--
GitLab