From d6b3209e437678e54cbfc69c9c2b38bf29897fba Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 23 Jul 2015 19:23:34 +0200
Subject: [PATCH] Fix test cases
---
.../frontends/passing/ImplicitDefs2.scala | 34 +++++++++----------
.../regression/repair/Compiler1.scala | 4 +--
.../resources/regression/repair/Heap4.scala | 2 +-
.../resources/regression/repair/List1.scala | 4 +--
.../regression/repair/MergeSort2.scala | 2 +-
.../regression/synthesis/Church/Add.scala | 4 +--
.../synthesis/Church/Distinct.scala | 4 +--
.../regression/synthesis/Church/Mult.scala | 4 +--
.../regression/synthesis/Church/Squared.scala | 4 +--
.../regression/synthesis/List/Delete.scala | 4 +--
.../regression/synthesis/List/Diff.scala | 4 +--
.../regression/synthesis/List/Insert.scala | 4 +--
.../regression/synthesis/List/Split1.scala | 4 +--
.../regression/synthesis/List/Split2.scala | 4 +--
.../regression/synthesis/List/Split3.scala | 4 +--
.../regression/synthesis/List/Union.scala | 4 +--
.../termination/looping/LambdaCalculus.scala | 4 +--
.../termination/looping/Queue.scala | 6 ++--
.../termination/valid/CountTowardsZero.scala | 4 +--
.../regression/termination/valid/Queue.scala | 4 +--
.../purescala/valid/ParBalance.scala | 4 +--
.../test/testcases/TestCasesCompile.scala | 16 +++++++--
testcases/repair/Compiler/Compiler.scala | 4 +--
testcases/repair/Compiler/Compiler1.scala | 4 +--
testcases/repair/Compiler/Compiler2.scala | 4 +--
testcases/repair/Compiler/Compiler3.scala | 4 +--
testcases/repair/Compiler/Compiler4.scala | 4 +--
testcases/repair/Compiler/Compiler5.scala | 4 +--
testcases/repair/Compiler/Compiler6.scala | 4 +--
testcases/repair/Heap/Heap.scala | 2 +-
testcases/repair/Heap/Heap1.scala | 2 +-
testcases/repair/Heap/Heap10.scala | 2 +-
testcases/repair/Heap/Heap2.scala | 2 +-
testcases/repair/Heap/Heap3.scala | 2 +-
testcases/repair/Heap/Heap4.scala | 2 +-
testcases/repair/Heap/Heap5.scala | 2 +-
testcases/repair/Heap/Heap6.scala | 2 +-
testcases/repair/Heap/Heap7.scala | 2 +-
testcases/repair/Heap/Heap8.scala | 2 +-
testcases/repair/Heap/Heap9.scala | 2 +-
testcases/repair/List/List.scala | 4 +--
testcases/repair/List/List1.scala | 4 +--
testcases/repair/List/List10.scala | 10 +++---
testcases/repair/List/List11.scala | 8 ++---
testcases/repair/List/List12.scala | 10 +++---
testcases/repair/List/List13.scala | 4 +--
testcases/repair/List/List2.scala | 4 +--
testcases/repair/List/List3.scala | 4 +--
testcases/repair/List/List4.scala | 6 ++--
testcases/repair/List/List5.scala | 6 ++--
testcases/repair/List/List6.scala | 6 ++--
testcases/repair/List/List7.scala | 10 +++---
testcases/repair/List/List8.scala | 10 +++---
testcases/repair/List/List9.scala | 10 +++---
testcases/repair/MergeSort/MergeSort.scala | 2 +-
testcases/repair/MergeSort/MergeSort1.scala | 2 +-
testcases/repair/MergeSort/MergeSort2.scala | 2 +-
testcases/repair/MergeSort/MergeSort3.scala | 2 +-
testcases/repair/MergeSort/MergeSort4.scala | 2 +-
testcases/repair/MergeSort/MergeSort5.scala | 2 +-
testcases/repair/PropLogic/PropLogic.scala | 2 +-
testcases/repair/PropLogic/PropLogic1.scala | 2 +-
testcases/repair/PropLogic/PropLogic2.scala | 2 +-
testcases/repair/PropLogic/PropLogic3.scala | 2 +-
testcases/repair/PropLogic/PropLogic4.scala | 2 +-
testcases/repair/PropLogic/PropLogic5.scala | 2 +-
testcases/repair/inria/FirstIndexOf.scala | 6 ++--
testcases/verification/Addresses.scala | 2 +-
.../higher-order/invalid/Lists2.scala | 2 +-
.../higher-order/valid/ListOps1.scala | 8 ++---
.../list-algorithms/TwoSizeFunctions.scala | 2 +-
testcases/verification/math/Fibonacci.scala | 4 +--
testcases/web/demos/02_Lists.scala | 2 +-
testcases/web/demos/03_Splits.scala | 2 +-
testcases/web/demos/05_OpenDays2.scala | 2 +-
testcases/web/sav15/03_Exercise3.scala | 6 ++--
testcases/web/sav15/05_Exercise5.scala | 10 +++---
testcases/web/sav15/06_Exercise6.scala | 4 +--
testcases/web/synthesis/01_List_Insert.scala | 4 +--
testcases/web/synthesis/02_List_Delete.scala | 4 +--
testcases/web/synthesis/03_List_Union.scala | 4 +--
testcases/web/synthesis/04_List_Diff.scala | 4 +--
testcases/web/synthesis/05_List_Split1.scala | 4 +--
testcases/web/synthesis/06_List_Split2.scala | 4 +--
testcases/web/synthesis/07_List_Split3.scala | 4 +--
.../web/synthesis/09_SortedList_Insert1.scala | 4 +--
.../web/synthesis/10_SortedList_Insert2.scala | 4 +--
.../web/synthesis/11_SortedList_Delete.scala | 4 +--
.../web/synthesis/12_SortedList_Diff.scala | 4 +--
.../synthesis/13_SortedList_InsertSort.scala | 4 +--
.../web/synthesis/14_SortedList_Union.scala | 4 +--
.../15_StrictSortedList_Insert.scala | 4 +--
.../16_StrictSortedList_Delete.scala | 4 +--
.../synthesis/17_StrictSortedList_Union.scala | 4 +--
.../web/synthesis/18_UnaryNumerals_Add.scala | 2 +-
.../synthesis/19_UnaryNumerals_Distinct.scala | 2 +-
.../web/synthesis/20_UnaryNumerals_Mult.scala | 2 +-
.../synthesis/21_UnaryNumerals_Squared.scala | 2 +-
.../web/verification/01_Amortized_Queue.scala | 2 +-
.../web/verification/03_Insertion_Sort.scala | 2 +-
.../web/verification/04_List_Operations.scala | 4 +--
.../web/verification/06_Red-Black_Tree.scala | 2 +-
.../verification/07_Search_Linked-List.scala | 6 ++--
.../web/verification/08_Sum_and_Max.scala | 4 +--
testcases/web/verification/14_HeapSort.scala | 4 +--
.../web/verification/15_LeftistHeap.scala | 6 ++--
106 files changed, 230 insertions(+), 220 deletions(-)
diff --git a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
index 9f4b1a83f..dba63890b 100644
--- a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
+++ b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
@@ -103,10 +103,10 @@ sealed abstract class List[T] {
} ensuring (res => (res.size == size) && (res.content == content))
def take(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
+ case (Nil(), _) => Nil[T]()
case (Cons(h, t), i) =>
if (i <= BigInt(0)) {
- Nil()
+ Nil[T]()
} else {
Cons(h, t.take(i-1))
}
@@ -117,7 +117,7 @@ sealed abstract class List[T] {
)}
def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
+ case (Nil(), _) => Nil[T]()
case (Cons(h, t), i) =>
if (i <= BigInt(0)) {
Cons(h, t)
@@ -136,7 +136,7 @@ sealed abstract class List[T] {
}
def replace(from: T, to: T): List[T] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
if (h == from) {
@@ -177,7 +177,7 @@ sealed abstract class List[T] {
case (Cons(h1, t1), Cons(h2, t2)) =>
Cons((h1, h2), t1.zip(t2))
case (_) =>
- Nil()
+ Nil[(T, B)]()
}} ensuring { _.size == (
if (this.size <= that.size) this.size else that.size
)}
@@ -190,7 +190,7 @@ sealed abstract class List[T] {
Cons(h, t - e)
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == this.content -- Set(e) }
def --(that: List[T]): List[T] = { this match {
@@ -201,7 +201,7 @@ sealed abstract class List[T] {
Cons(h, t -- that)
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == this.content -- that.content }
def &(that: List[T]): List[T] = { this match {
@@ -212,7 +212,7 @@ sealed abstract class List[T] {
t & that
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == (this.content & that.content) }
def pad(s: BigInt, e: T): List[T] = (this, s) match {
@@ -225,13 +225,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h == e) {
- Some(0)
+ Some[BigInt](0)
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i+1)
}
}
@@ -350,7 +350,7 @@ sealed abstract class List[T] {
// Higher-order API
def map[R](f: T => R): List[R] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[R]()
case Cons(h, t) => f(h) :: t.map(f)
}} ensuring { _.size == this.size}
@@ -365,12 +365,12 @@ sealed abstract class List[T] {
}
def scanLeft[R](z: R)(f: (R,T) => R): List[R] = this match {
- case Nil() => z :: Nil()
+ case Nil() => z :: Nil[R]()
case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
}
def scanRight[R](f: (T,R) => R)(z: R): List[R] = { this match {
- case Nil() => z :: Nil()
+ case Nil() => z :: Nil[R]()
case Cons(h, t) =>
val rest@Cons(h1,_) = t.scanRight(f)(z)
f(h, h1) :: rest
@@ -380,7 +380,7 @@ sealed abstract class List[T] {
ListOps.flatten(this map f)
def filter(p: T => Boolean): List[T] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(h, t) if p(h) => Cons(h, t.filter(p))
case Cons(_, t) => t.filter(p)
}} ensuring { res => res.size <= this.size && res.forall(p) }
@@ -396,7 +396,7 @@ sealed abstract class List[T] {
def exists(p: T => Boolean) = !forall(!p(_))
def find(p: T => Boolean): Option[T] = { this match {
- case Nil() => None()
+ case Nil() => None[T]()
case Cons(h, t) if p(h) => Some(h)
case Cons(_, t) => t.find(p)
}} ensuring { _.isDefined == exists(p) }
@@ -426,7 +426,7 @@ object List {
object ListOps {
def flatten[T](ls: List[List[T]]): List[T] = ls match {
case Cons(h, t) => h ++ flatten(t)
- case Nil() => Nil()
+ case Nil() => Nil[T]()
}
def isSorted(ls: List[BigInt]): Boolean = ls match {
diff --git a/src/test/resources/regression/repair/Compiler1.scala b/src/test/resources/regression/repair/Compiler1.scala
index 9ff0785d7..300868d67 100644
--- a/src/test/resources/regression/repair/Compiler1.scala
+++ b/src/test/resources/regression/repair/Compiler1.scala
@@ -110,9 +110,9 @@ object Semantics {
def semUntyped(t : Expr): BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/src/test/resources/regression/repair/Heap4.scala b/src/test/resources/regression/repair/Heap4.scala
index 01c8b41f9..937e29b5c 100644
--- a/src/test/resources/regression/repair/Heap4.scala
+++ b/src/test/resources/regression/repair/Heap4.scala
@@ -47,7 +47,7 @@ object HeapSort {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/src/test/resources/regression/repair/List1.scala b/src/test/resources/regression/repair/List1.scala
index ff31089cf..79b7ecb44 100644
--- a/src/test/resources/regression/repair/List1.scala
+++ b/src/test/resources/regression/repair/List1.scala
@@ -9,8 +9,8 @@ import leon.collection._
sealed abstract class List0[T] {
def size: BigInt = (this match {
- case Nil0() => 0
- case Cons0(h, t) => 1 + t.size
+ case Nil0() => BigInt(0)
+ case Cons0(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/src/test/resources/regression/repair/MergeSort2.scala b/src/test/resources/regression/repair/MergeSort2.scala
index 649582ee2..4447edc40 100644
--- a/src/test/resources/regression/repair/MergeSort2.scala
+++ b/src/test/resources/regression/repair/MergeSort2.scala
@@ -9,7 +9,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
index 5931eeb59..c94fc4c7f 100644
--- a/src/test/resources/regression/synthesis/Church/Add.scala
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
index a6fb4881c..b7f093e9f 100644
--- a/src/test/resources/regression/synthesis/Church/Distinct.scala
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
index 9f8f422c6..bc4afe213 100644
--- a/src/test/resources/regression/synthesis/Church/Mult.scala
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index 5d7877469..92ac747b8 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n:Num) : BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
index 07d64d6b3..0c82b3da4 100644
--- a/src/test/resources/regression/synthesis/List/Delete.scala
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -10,8 +10,8 @@ object Delete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
index 8659cd59b..477ea0bdb 100644
--- a/src/test/resources/regression/synthesis/List/Diff.scala
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -10,8 +10,8 @@ object Diff {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index 13636c155..c98947bb1 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -10,8 +10,8 @@ object Insert {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Split1.scala b/src/test/resources/regression/synthesis/List/Split1.scala
index facbda843..66def0ffa 100644
--- a/src/test/resources/regression/synthesis/List/Split1.scala
+++ b/src/test/resources/regression/synthesis/List/Split1.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Split2.scala b/src/test/resources/regression/synthesis/List/Split2.scala
index 38c07caf5..5d66b4a59 100644
--- a/src/test/resources/regression/synthesis/List/Split2.scala
+++ b/src/test/resources/regression/synthesis/List/Split2.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Split3.scala b/src/test/resources/regression/synthesis/List/Split3.scala
index 15c74190e..eca76884d 100644
--- a/src/test/resources/regression/synthesis/List/Split3.scala
+++ b/src/test/resources/regression/synthesis/List/Split3.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
index 79d97ee9f..c36a5933c 100644
--- a/src/test/resources/regression/synthesis/List/Union.scala
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -10,8 +10,8 @@ object Union {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/termination/looping/LambdaCalculus.scala b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
index 884e5dee5..d24d8c31b 100644
--- a/src/test/resources/regression/termination/looping/LambdaCalculus.scala
+++ b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
@@ -32,9 +32,9 @@ object LambdaCalculus {
case App(t1, t2) => looping_eval(t1) match {
case Some(Abs(x, body)) => looping_eval(t2) match {
case Some(v2) => looping_eval(subst(x, v2, body))
- case None() => None()
+ case None() => None[Term]()
}
- case _ => None() // stuck
+ case _ => None[Term]() // stuck
}
case _ => Some(t) // Abs or Var, already a value
}) ensuring { res => res match {
diff --git a/src/test/resources/regression/termination/looping/Queue.scala b/src/test/resources/regression/termination/looping/Queue.scala
index a571e82e8..3df1a9ac5 100644
--- a/src/test/resources/regression/termination/looping/Queue.scala
+++ b/src/test/resources/regression/termination/looping/Queue.scala
@@ -7,19 +7,19 @@ sealed abstract class Queue[T] {
def looping_1: BigInt = {
this match {
- case QEmpty() => 0
+ case QEmpty() => BigInt(0)
case QCons(f, r) => f.size + r.size
}
} ensuring (res => res == this.looping_2.size && res >= 0)
def looping_2: List[T] = (this match {
- case QEmpty() => Nil()
+ case QEmpty() => Nil[T]()
case QCons(f, r) => f ++ r.reverse
}) ensuring (resOne => this.looping_3 == resOne.content && resOne.size == this.looping_1 && resOne.size >= 0)
def looping_3: Set[T] = (this match {
- case QEmpty() => Set()
+ case QEmpty() => Set[T]()
case QCons(f, r) => f.content ++ r.content
}) ensuring (res => res == this.looping_2.content)
}
diff --git a/src/test/resources/regression/termination/valid/CountTowardsZero.scala b/src/test/resources/regression/termination/valid/CountTowardsZero.scala
index 4ef5ba8b0..e0ce187ad 100644
--- a/src/test/resources/regression/termination/valid/CountTowardsZero.scala
+++ b/src/test/resources/regression/termination/valid/CountTowardsZero.scala
@@ -2,13 +2,13 @@
object Test {
def f(x: BigInt): BigInt = {
if (x == 0) {
- 0
+ BigInt(0)
} else if (x > 0) {
f(x-1)+2
} else if (x < 0) {
f(x+1)-2
} else {
- 33
+ BigInt(33)
}
} ensuring (_ == x*2)
}
diff --git a/src/test/resources/regression/termination/valid/Queue.scala b/src/test/resources/regression/termination/valid/Queue.scala
index 2b73919a7..dee019a41 100644
--- a/src/test/resources/regression/termination/valid/Queue.scala
+++ b/src/test/resources/regression/termination/valid/Queue.scala
@@ -7,13 +7,13 @@ sealed abstract class Queue[T] {
def size: BigInt = {
this match {
- case QEmpty() => 0
+ case QEmpty() => BigInt(0)
case QCons(f, r) => f.size + r.size
}
} ensuring (res => res == this.toList.size && res >= 0)
def toList: List[T] = (this match {
- case QEmpty() => Nil()
+ case QEmpty() => Nil[T]()
case QCons(f, r) => f ++ r.reverse
}) ensuring (resOne => this.content == resOne.content && resOne.size >= 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
index 4db8aecb0..29133762e 100644
--- a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
@@ -147,8 +147,8 @@ object ParBalance {
}
def size(list: List): BigInt = (list match {
- case Nil() => 0
- case Cons(h, t) => 1 + size(t)
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + size(t)
}) ensuring (_ >= 0)
def addLast(list: List, x: BigInt): List = {
diff --git a/src/test/scala/leon/test/testcases/TestCasesCompile.scala b/src/test/scala/leon/test/testcases/TestCasesCompile.scala
index b5fe1ca32..f82ff346c 100644
--- a/src/test/scala/leon/test/testcases/TestCasesCompile.scala
+++ b/src/test/scala/leon/test/testcases/TestCasesCompile.scala
@@ -13,7 +13,7 @@ class TestCasesCompile extends LeonTestSuite {
val pipeline = frontends.scalac.ExtractionPhase andThen utils.PreprocessingPhase
- def testFrontend(f: File, strip: Int) = {
+ def testFrontend(f: File, strip: Int): Boolean = {
val name = f.getAbsolutePath.split("/").toList.drop(strip).mkString("/")
val ctx = createLeonContext()
@@ -21,9 +21,11 @@ class TestCasesCompile extends LeonTestSuite {
try {
pipeline.run(ctx)(List(f.getAbsolutePath))
info(name)
+ true
} catch {
case _: LeonFatalError =>
- fail("Failed to compile "+name)
+ info(Console.YELLOW+" Failed to compile "+name)
+ false
}
}
@@ -46,8 +48,16 @@ class TestCasesCompile extends LeonTestSuite {
info("Compiling "+all.size+" testcases...")
+ var nFailed = new java.util.concurrent.atomic.AtomicInteger(0)
all.par.foreach { f =>
- testFrontend(f, slashes)
+ if (!testFrontend(f, slashes)) {
+ nFailed.incrementAndGet()
+ }
+ }
+
+ val nFailedInt = nFailed.get()
+ if (nFailedInt > 0) {
+ fail(s"$nFailedInt test(s) failed to compile")
}
}
}
diff --git a/testcases/repair/Compiler/Compiler.scala b/testcases/repair/Compiler/Compiler.scala
index f0d0ed1f0..4b77a547a 100644
--- a/testcases/repair/Compiler/Compiler.scala
+++ b/testcases/repair/Compiler/Compiler.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler1.scala b/testcases/repair/Compiler/Compiler1.scala
index f3e840442..b1f9bc859 100644
--- a/testcases/repair/Compiler/Compiler1.scala
+++ b/testcases/repair/Compiler/Compiler1.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler2.scala b/testcases/repair/Compiler/Compiler2.scala
index 6703cf715..1950b679a 100644
--- a/testcases/repair/Compiler/Compiler2.scala
+++ b/testcases/repair/Compiler/Compiler2.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler3.scala b/testcases/repair/Compiler/Compiler3.scala
index 24937f81a..367e43b9f 100644
--- a/testcases/repair/Compiler/Compiler3.scala
+++ b/testcases/repair/Compiler/Compiler3.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
index 33f24376e..f49670ddc 100644
--- a/testcases/repair/Compiler/Compiler4.scala
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler5.scala b/testcases/repair/Compiler/Compiler5.scala
index 5ce706212..fdefc6b31 100644
--- a/testcases/repair/Compiler/Compiler5.scala
+++ b/testcases/repair/Compiler/Compiler5.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
index 0848603a1..44bf523ec 100644
--- a/testcases/repair/Compiler/Compiler6.scala
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Heap/Heap.scala b/testcases/repair/Heap/Heap.scala
index 71f18a760..a3c064376 100644
--- a/testcases/repair/Heap/Heap.scala
+++ b/testcases/repair/Heap/Heap.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap1.scala b/testcases/repair/Heap/Heap1.scala
index bb6294030..7cd865961 100644
--- a/testcases/repair/Heap/Heap1.scala
+++ b/testcases/repair/Heap/Heap1.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap10.scala b/testcases/repair/Heap/Heap10.scala
index bba2389a3..de5ae51d1 100644
--- a/testcases/repair/Heap/Heap10.scala
+++ b/testcases/repair/Heap/Heap10.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap2.scala b/testcases/repair/Heap/Heap2.scala
index 75f53a963..175f55d19 100644
--- a/testcases/repair/Heap/Heap2.scala
+++ b/testcases/repair/Heap/Heap2.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala
index b24024ea7..5b9fadeeb 100644
--- a/testcases/repair/Heap/Heap3.scala
+++ b/testcases/repair/Heap/Heap3.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap4.scala b/testcases/repair/Heap/Heap4.scala
index d277fde61..f6176a56a 100644
--- a/testcases/repair/Heap/Heap4.scala
+++ b/testcases/repair/Heap/Heap4.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap5.scala b/testcases/repair/Heap/Heap5.scala
index fcddb9e08..5bbccada5 100644
--- a/testcases/repair/Heap/Heap5.scala
+++ b/testcases/repair/Heap/Heap5.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap6.scala b/testcases/repair/Heap/Heap6.scala
index aa9eb7230..2760af2fa 100644
--- a/testcases/repair/Heap/Heap6.scala
+++ b/testcases/repair/Heap/Heap6.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap7.scala b/testcases/repair/Heap/Heap7.scala
index 91baf66c4..b2232fa7b 100644
--- a/testcases/repair/Heap/Heap7.scala
+++ b/testcases/repair/Heap/Heap7.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap8.scala b/testcases/repair/Heap/Heap8.scala
index 0d21fc368..3debf1630 100644
--- a/testcases/repair/Heap/Heap8.scala
+++ b/testcases/repair/Heap/Heap8.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap9.scala b/testcases/repair/Heap/Heap9.scala
index 0a9197a34..4ed28b867 100644
--- a/testcases/repair/Heap/Heap9.scala
+++ b/testcases/repair/Heap/Heap9.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/List/List.scala b/testcases/repair/List/List.scala
index 3f1e65814..5f95f7595 100644
--- a/testcases/repair/List/List.scala
+++ b/testcases/repair/List/List.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala
index 53a496055..86910a604 100644
--- a/testcases/repair/List/List1.scala
+++ b/testcases/repair/List/List1.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List10.scala b/testcases/repair/List/List10.scala
index edef652eb..61751947d 100644
--- a/testcases/repair/List/List10.scala
+++ b/testcases/repair/List/List10.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 3 + t.size //FIXME
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(3) + t.size //FIXME
}) ensuring { (this, _) passes {
case Cons(_, Nil()) => 1
case Nil() => 0
@@ -143,7 +143,7 @@ sealed abstract class List[T] {
Cons(h, t - e)
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def --(that: List[T]): List[T] = this match {
@@ -154,7 +154,7 @@ sealed abstract class List[T] {
Cons(h, t -- that)
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def &(that: List[T]): List[T] = this match {
@@ -165,7 +165,7 @@ sealed abstract class List[T] {
t & that
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def pad(s: BigInt, e: T): List[T] = { (this, s) match {
diff --git a/testcases/repair/List/List11.scala b/testcases/repair/List/List11.scala
index 12eb4c6a1..01ea11450 100644
--- a/testcases/repair/List/List11.scala
+++ b/testcases/repair/List/List11.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -331,8 +331,8 @@ object ListOps {
}
def sum(l: List[BigInt]): BigInt = { l match {
- case Nil() => 0
- case Cons(x, xs) => 1 + sum(xs) // FIXME
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => BigInt(1) + sum(xs) // FIXME
}} ensuring { (l, _) passes {
case Cons(a, Nil()) => a
case Cons(a, Cons(b, Nil())) => a + b
diff --git a/testcases/repair/List/List12.scala b/testcases/repair/List/List12.scala
index 1774d1efd..eeada312b 100644
--- a/testcases/repair/List/List12.scala
+++ b/testcases/repair/List/List12.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -140,7 +140,7 @@ sealed abstract class List[T] {
Cons(h, t - e)
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == this.content -- Set(e) }
@@ -152,7 +152,7 @@ sealed abstract class List[T] {
Cons(h, t -- that)
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def &(that: List[T]): List[T] = this match {
@@ -163,7 +163,7 @@ sealed abstract class List[T] {
t & that
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def pad(s: BigInt, e: T): List[T] = { (this, s) match {
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index 96dc9abcc..dec461f0a 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List2.scala b/testcases/repair/List/List2.scala
index e5c850130..77fa7f0f9 100644
--- a/testcases/repair/List/List2.scala
+++ b/testcases/repair/List/List2.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List3.scala b/testcases/repair/List/List3.scala
index 8fc99b7d2..5624d7db9 100644
--- a/testcases/repair/List/List3.scala
+++ b/testcases/repair/List/List3.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index d48256fe0..0e0aad1ee 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -79,7 +79,7 @@ sealed abstract class List[T] {
}
def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
+ case (Nil(), _) => Nil[T]()
case (Cons(h, t), i) =>
// FIXME
//if (i == 0) {
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 471bff800..2e8099bce 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -94,7 +94,7 @@ sealed abstract class List[T] {
}
def replace(from: T, to: T): List[T] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
//if (h == from) { FIXME
diff --git a/testcases/repair/List/List6.scala b/testcases/repair/List/List6.scala
index f7881ff1e..1cf527cfa 100644
--- a/testcases/repair/List/List6.scala
+++ b/testcases/repair/List/List6.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -242,7 +242,7 @@ sealed abstract class List[T] {
t.count(e)
}
case Nil() =>
- 0
+ BigInt(0)
}} ensuring {((this, e), _) passes {
case (Cons(a, Cons(b, Cons(a1, Cons(b2, Nil())))), a2) if a == a1 && a == a2 && b != a2 && b2 != a2 => 2
case (Cons(a, Cons(b, Nil())), c) if a != c && b != c => 0
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index a67f7e5c4..4a2d34262 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -179,13 +179,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h == e) {
- Some(0)
+ Some(BigInt(0))
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i) // FIXME forgot +1
}
}
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index 0204d4f52..3d79f0434 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -179,13 +179,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h == e) {
- Some(0)
+ Some(BigInt(0))
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i+2) // FIXME +1
}
}
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index 176cb595f..c9d528a94 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -179,13 +179,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h != e) { // FIXME
- Some(0)
+ Some(BigInt(0))
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i + 1)
}
}
diff --git a/testcases/repair/MergeSort/MergeSort.scala b/testcases/repair/MergeSort/MergeSort.scala
index aac638b9a..1ce4210a5 100644
--- a/testcases/repair/MergeSort/MergeSort.scala
+++ b/testcases/repair/MergeSort/MergeSort.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
index bef7f2391..88b031908 100644
--- a/testcases/repair/MergeSort/MergeSort1.scala
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(rec1, rec2) // FIXME: Forgot a,b
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort2.scala b/testcases/repair/MergeSort/MergeSort2.scala
index 11c3a1cdb..5c186eca7 100644
--- a/testcases/repair/MergeSort/MergeSort2.scala
+++ b/testcases/repair/MergeSort/MergeSort2.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort3.scala b/testcases/repair/MergeSort/MergeSort3.scala
index 3d9c8192a..ec37db65c 100644
--- a/testcases/repair/MergeSort/MergeSort3.scala
+++ b/testcases/repair/MergeSort/MergeSort3.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort4.scala b/testcases/repair/MergeSort/MergeSort4.scala
index 4422402b1..5c3479844 100644
--- a/testcases/repair/MergeSort/MergeSort4.scala
+++ b/testcases/repair/MergeSort/MergeSort4.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort5.scala b/testcases/repair/MergeSort/MergeSort5.scala
index 1bf9d50ce..7746d23c7 100644
--- a/testcases/repair/MergeSort/MergeSort5.scala
+++ b/testcases/repair/MergeSort/MergeSort5.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/PropLogic/PropLogic.scala b/testcases/repair/PropLogic/PropLogic.scala
index 2819234ff..a03dd35b4 100644
--- a/testcases/repair/PropLogic/PropLogic.scala
+++ b/testcases/repair/PropLogic/PropLogic.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic1.scala b/testcases/repair/PropLogic/PropLogic1.scala
index 93cd6bfbf..a27d3afe5 100644
--- a/testcases/repair/PropLogic/PropLogic1.scala
+++ b/testcases/repair/PropLogic/PropLogic1.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic2.scala b/testcases/repair/PropLogic/PropLogic2.scala
index 2819234ff..a03dd35b4 100644
--- a/testcases/repair/PropLogic/PropLogic2.scala
+++ b/testcases/repair/PropLogic/PropLogic2.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic3.scala b/testcases/repair/PropLogic/PropLogic3.scala
index 8f2a62cd8..87d78dbc9 100644
--- a/testcases/repair/PropLogic/PropLogic3.scala
+++ b/testcases/repair/PropLogic/PropLogic3.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic4.scala b/testcases/repair/PropLogic/PropLogic4.scala
index 40cddee80..29e1c5783 100644
--- a/testcases/repair/PropLogic/PropLogic4.scala
+++ b/testcases/repair/PropLogic/PropLogic4.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic5.scala b/testcases/repair/PropLogic/PropLogic5.scala
index 6b24d9926..e89e2c5ae 100644
--- a/testcases/repair/PropLogic/PropLogic5.scala
+++ b/testcases/repair/PropLogic/PropLogic5.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/inria/FirstIndexOf.scala b/testcases/repair/inria/FirstIndexOf.scala
index 2693d18cd..3239632e4 100644
--- a/testcases/repair/inria/FirstIndexOf.scala
+++ b/testcases/repair/inria/FirstIndexOf.scala
@@ -6,15 +6,15 @@ import leon.lang.synthesis._
object FirstIndexOf {
def firstIndexOf(l: List[Int], v: Int): BigInt = {
l match {
- case Cons(h, t) if v == h => 0
+ case Cons(h, t) if v == h => BigInt(0)
case Cons(h, t) =>
if (firstIndexOf(t, v) >= 0) {
firstIndexOf(t, v)+1
} else {
- -1
+ BigInt(-1)
}
case Nil() =>
- -1
+ BigInt(-1)
}
} ensuring {
(res: BigInt) => (if (l.content contains v) {
diff --git a/testcases/verification/Addresses.scala b/testcases/verification/Addresses.scala
index 4eebe934f..b6f356fe2 100644
--- a/testcases/verification/Addresses.scala
+++ b/testcases/verification/Addresses.scala
@@ -55,7 +55,7 @@ object Addresses {
def max(x:BigInt,y:BigInt) = if (x <= y) x else y
def collectA(x:BigInt,l:List) : (BigInt,BigInt,List) = (l match {
- case Nil() => (0,0,Nil())
+ case Nil() => (BigInt(0),BigInt(0),Nil())
case Cons(a,b,c,l1) if (a==x) => {
val (b2,c2,l2) = collectA(x,l1)
(max(b,b2),max(c,c2),l2)
diff --git a/testcases/verification/higher-order/invalid/Lists2.scala b/testcases/verification/higher-order/invalid/Lists2.scala
index 59faa779b..29285c8a9 100644
--- a/testcases/verification/higher-order/invalid/Lists2.scala
+++ b/testcases/verification/higher-order/invalid/Lists2.scala
@@ -35,7 +35,7 @@ object Lists2 {
val (tres, sres) = bubble(t1)
(Cons(h1, tres), sres)
case Nil() =>
- (Nil(), false)
+ (Nil[A](), false)
}
} ensuring { _ match {
/*res =>
diff --git a/testcases/verification/higher-order/valid/ListOps1.scala b/testcases/verification/higher-order/valid/ListOps1.scala
index 59903df08..8d02e9bea 100644
--- a/testcases/verification/higher-order/valid/ListOps1.scala
+++ b/testcases/verification/higher-order/valid/ListOps1.scala
@@ -33,7 +33,7 @@ object ListOps1 {
case Some(b) => Cons(b, collect(f, t))
case None() => collect(f, t)
}
- case Nil() => Nil()
+ case Nil() => Nil[B]()
}
} ensuring {
res => res.size <= l.size
@@ -43,7 +43,7 @@ object ListOps1 {
l match {
case Cons(h, t) =>
f(h).orElse(collectFirst(f, t))
- case Nil() => None()
+ case Nil() => None[B]()
}
} ensuring {
res => !l.isEmpty || res.isEmpty
@@ -64,7 +64,7 @@ object ListOps1 {
l match {
case Cons(h, t) if f(h) => dropWhile(f, t)
case Cons(h, t) if !f(h) => l
- case Nil() => Nil()
+ case Nil() => Nil[A]()
}
} ensuring {
res =>
@@ -103,7 +103,7 @@ object ListOps1 {
def mapWitness[A,B](f: A => B, l: List[A], w: A): List[B] = {
l match {
case Cons(h, t) => f(h) :: mapWitness(f, t, w)
- case Nil() => Nil()
+ case Nil() => Nil[B]()
}
} ensuring {
res => if (l.content contains w) res.content contains f(w) else true
diff --git a/testcases/verification/list-algorithms/TwoSizeFunctions.scala b/testcases/verification/list-algorithms/TwoSizeFunctions.scala
index b5583a707..b28e54561 100644
--- a/testcases/verification/list-algorithms/TwoSizeFunctions.scala
+++ b/testcases/verification/list-algorithms/TwoSizeFunctions.scala
@@ -8,7 +8,7 @@ object TwoSizeFunctions {
def size1(l: List) : BigInt = (l match {
case Cons(_, xs) => size1(xs) + 1
- case Nil() => 0
+ case Nil() => BigInt(0)
}) ensuring(_ >= 0)
def size2(l: List) : BigInt = size2acc(l, 0)
diff --git a/testcases/verification/math/Fibonacci.scala b/testcases/verification/math/Fibonacci.scala
index df2b731c5..82e3483db 100644
--- a/testcases/verification/math/Fibonacci.scala
+++ b/testcases/verification/math/Fibonacci.scala
@@ -18,7 +18,7 @@ object Fibonacci {
def f(n : BigInt) : BigInt = {
require(n >= 0)
if(n <= 0)
- 1
+ BigInt(1)
else
f(n-1) + g(n-1)
}
@@ -26,7 +26,7 @@ object Fibonacci {
def g(n : BigInt) : BigInt = {
require(n >= 0)
if(n <= 0)
- 1
+ BigInt(1)
else
f(n-1)
} ensuring(_ == fib(n + 1))
diff --git a/testcases/web/demos/02_Lists.scala b/testcases/web/demos/02_Lists.scala
index f4abad115..59d3175ba 100644
--- a/testcases/web/demos/02_Lists.scala
+++ b/testcases/web/demos/02_Lists.scala
@@ -8,7 +8,7 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
diff --git a/testcases/web/demos/03_Splits.scala b/testcases/web/demos/03_Splits.scala
index 740dc34a8..a2bb904d0 100644
--- a/testcases/web/demos/03_Splits.scala
+++ b/testcases/web/demos/03_Splits.scala
@@ -8,7 +8,7 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
diff --git a/testcases/web/demos/05_OpenDays2.scala b/testcases/web/demos/05_OpenDays2.scala
index c092735fa..480d02080 100644
--- a/testcases/web/demos/05_OpenDays2.scala
+++ b/testcases/web/demos/05_OpenDays2.scala
@@ -40,7 +40,7 @@ object EpflOpenDays {
sealed abstract class Liste {
def somme: BigInt = {
this match {
- case Vide => 0
+ case Vide => BigInt(0)
case Elem(p, reste) => p.valeur + reste.somme
}
} ensuring { _ >= 0 }
diff --git a/testcases/web/sav15/03_Exercise3.scala b/testcases/web/sav15/03_Exercise3.scala
index 4dff97756..ca9d23efb 100644
--- a/testcases/web/sav15/03_Exercise3.scala
+++ b/testcases/web/sav15/03_Exercise3.scala
@@ -6,7 +6,7 @@ object ListWithSize {
def size: BigInt = {
this match {
case Cons(h, t) => 1 + t.size
- case Nil() => 0
+ case Nil() => BigInt(0)
}
} // TODO: Add appropriate post-condition
@@ -24,7 +24,7 @@ object ListWithSize {
def zip[U](that: List[U]): List[(T, U)] = {
// TODO: Add appropriate pre-condition
this match {
- case Nil() => Nil()
+ case Nil() => Nil[(T,U)]()
case Cons(h1, t1) => that match {
case Cons(h2, t2) => Cons((h1, h2), t1.zip(t2))
}
@@ -70,7 +70,7 @@ object ListWithSize {
}.holds
def drunk[T](l: List[T]): List[T] = (l match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
}) ensuring {
res => true // TODO: find postcondition
diff --git a/testcases/web/sav15/05_Exercise5.scala b/testcases/web/sav15/05_Exercise5.scala
index 787ab6de2..a76401c26 100644
--- a/testcases/web/sav15/05_Exercise5.scala
+++ b/testcases/web/sav15/05_Exercise5.scala
@@ -5,7 +5,7 @@ object SearchList {
sealed abstract class List[T] {
def size: BigInt = {
this match {
- case Nil() => 0
+ case Nil() => BigInt(0)
case Cons(h, t) => 1 + t.size
}
} ensuring { _ >= 0 }
@@ -19,8 +19,8 @@ object SearchList {
def firstPosOf(v: T): BigInt = {
this match {
- case Nil() => -1
- case Cons(h, t) if h == v => 0
+ case Nil() => BigInt(-1)
+ case Cons(h, t) if h == v => BigInt(0)
case Cons(h, t) =>
val p = t.firstPosOf(v)
if (p >= 0) {
@@ -37,8 +37,8 @@ object SearchList {
def take(n: BigInt): List[T] = {
require(n >= 0)
this match {
- case Nil() => Nil()
- case Cons(h, t) if n == 0 => Nil()
+ case Nil() => Nil[T]()
+ case Cons(h, t) if n == 0 => Nil[T]()
case Cons(h, t) => Cons(h, t.take(n - 1))
}
} ensuring {
diff --git a/testcases/web/sav15/06_Exercise6.scala b/testcases/web/sav15/06_Exercise6.scala
index 636abaca0..01aa1d62a 100644
--- a/testcases/web/sav15/06_Exercise6.scala
+++ b/testcases/web/sav15/06_Exercise6.scala
@@ -26,7 +26,7 @@ object BinaryTree {
def size: BigInt = {
this match {
- case Empty => 0
+ case Empty => BigInt(0)
case Node(l, _, r) => l.size + r.size + 1
}
} ensuring { _ >= 0 }
@@ -68,7 +68,7 @@ object BinaryTree {
def toList: List[BigInt] = {
require(isBT)
- Nil() // TODO
+ Nil[BigInt]() // TODO
} ensuring {
res => res.content == this.content && isSorted(res)
}
diff --git a/testcases/web/synthesis/01_List_Insert.scala b/testcases/web/synthesis/01_List_Insert.scala
index 62e91d9b9..40b7b0c74 100644
--- a/testcases/web/synthesis/01_List_Insert.scala
+++ b/testcases/web/synthesis/01_List_Insert.scala
@@ -8,8 +8,8 @@ object Insert {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/02_List_Delete.scala b/testcases/web/synthesis/02_List_Delete.scala
index a548f46e2..8230af747 100644
--- a/testcases/web/synthesis/02_List_Delete.scala
+++ b/testcases/web/synthesis/02_List_Delete.scala
@@ -8,8 +8,8 @@ object Delete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/03_List_Union.scala b/testcases/web/synthesis/03_List_Union.scala
index 0b21dc037..b03d4e5a2 100644
--- a/testcases/web/synthesis/03_List_Union.scala
+++ b/testcases/web/synthesis/03_List_Union.scala
@@ -8,8 +8,8 @@ object Union {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/04_List_Diff.scala b/testcases/web/synthesis/04_List_Diff.scala
index 0943955b1..775d44083 100644
--- a/testcases/web/synthesis/04_List_Diff.scala
+++ b/testcases/web/synthesis/04_List_Diff.scala
@@ -8,8 +8,8 @@ object Diff {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/05_List_Split1.scala b/testcases/web/synthesis/05_List_Split1.scala
index facbda843..1838a6bb0 100644
--- a/testcases/web/synthesis/05_List_Split1.scala
+++ b/testcases/web/synthesis/05_List_Split1.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/06_List_Split2.scala b/testcases/web/synthesis/06_List_Split2.scala
index 38c07caf5..0b917467f 100644
--- a/testcases/web/synthesis/06_List_Split2.scala
+++ b/testcases/web/synthesis/06_List_Split2.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/07_List_Split3.scala b/testcases/web/synthesis/07_List_Split3.scala
index 15c74190e..8a7897ebb 100644
--- a/testcases/web/synthesis/07_List_Split3.scala
+++ b/testcases/web/synthesis/07_List_Split3.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/09_SortedList_Insert1.scala b/testcases/web/synthesis/09_SortedList_Insert1.scala
index affc5b455..891c55cae 100644
--- a/testcases/web/synthesis/09_SortedList_Insert1.scala
+++ b/testcases/web/synthesis/09_SortedList_Insert1.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/10_SortedList_Insert2.scala b/testcases/web/synthesis/10_SortedList_Insert2.scala
index e44eac286..a199c7f28 100644
--- a/testcases/web/synthesis/10_SortedList_Insert2.scala
+++ b/testcases/web/synthesis/10_SortedList_Insert2.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/11_SortedList_Delete.scala b/testcases/web/synthesis/11_SortedList_Delete.scala
index 31305ca09..1438555d1 100644
--- a/testcases/web/synthesis/11_SortedList_Delete.scala
+++ b/testcases/web/synthesis/11_SortedList_Delete.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/12_SortedList_Diff.scala b/testcases/web/synthesis/12_SortedList_Diff.scala
index 9e4e32bae..33d5dc693 100644
--- a/testcases/web/synthesis/12_SortedList_Diff.scala
+++ b/testcases/web/synthesis/12_SortedList_Diff.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/13_SortedList_InsertSort.scala b/testcases/web/synthesis/13_SortedList_InsertSort.scala
index 8f5b78247..5f4076ac0 100644
--- a/testcases/web/synthesis/13_SortedList_InsertSort.scala
+++ b/testcases/web/synthesis/13_SortedList_InsertSort.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/14_SortedList_Union.scala b/testcases/web/synthesis/14_SortedList_Union.scala
index 95d17bb61..a5c4de9c6 100644
--- a/testcases/web/synthesis/14_SortedList_Union.scala
+++ b/testcases/web/synthesis/14_SortedList_Union.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/15_StrictSortedList_Insert.scala b/testcases/web/synthesis/15_StrictSortedList_Insert.scala
index 6c7543ad3..378ae688e 100644
--- a/testcases/web/synthesis/15_StrictSortedList_Insert.scala
+++ b/testcases/web/synthesis/15_StrictSortedList_Insert.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/16_StrictSortedList_Delete.scala b/testcases/web/synthesis/16_StrictSortedList_Delete.scala
index 81827ed03..6a79ccc11 100644
--- a/testcases/web/synthesis/16_StrictSortedList_Delete.scala
+++ b/testcases/web/synthesis/16_StrictSortedList_Delete.scala
@@ -8,8 +8,8 @@ object Delete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/17_StrictSortedList_Union.scala b/testcases/web/synthesis/17_StrictSortedList_Union.scala
index cf2fcd727..c4e7d45e0 100644
--- a/testcases/web/synthesis/17_StrictSortedList_Union.scala
+++ b/testcases/web/synthesis/17_StrictSortedList_Union.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/18_UnaryNumerals_Add.scala b/testcases/web/synthesis/18_UnaryNumerals_Add.scala
index 694f76a15..7bf58114b 100644
--- a/testcases/web/synthesis/18_UnaryNumerals_Add.scala
+++ b/testcases/web/synthesis/18_UnaryNumerals_Add.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala b/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
index 827d8d70f..d41ef8a03 100644
--- a/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
+++ b/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/synthesis/20_UnaryNumerals_Mult.scala b/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
index 1e58606d0..800812e57 100644
--- a/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
+++ b/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/synthesis/21_UnaryNumerals_Squared.scala b/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
index d660c247e..9dd48fbc1 100644
--- a/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
+++ b/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n:Num) : BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/verification/01_Amortized_Queue.scala b/testcases/web/verification/01_Amortized_Queue.scala
index e8190385a..e67f9c4c9 100644
--- a/testcases/web/verification/01_Amortized_Queue.scala
+++ b/testcases/web/verification/01_Amortized_Queue.scala
@@ -10,7 +10,7 @@ object AmortizedQueue {
case class Queue(front : List, rear : List) extends AbsQueue
def size(list : List) : BigInt = (list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/03_Insertion_Sort.scala b/testcases/web/verification/03_Insertion_Sort.scala
index a3a81d753..e53b89b17 100644
--- a/testcases/web/verification/03_Insertion_Sort.scala
+++ b/testcases/web/verification/03_Insertion_Sort.scala
@@ -11,7 +11,7 @@ object InsertionSort {
case object None extends OptInt
def size(l : List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/04_List_Operations.scala b/testcases/web/verification/04_List_Operations.scala
index f7e6d590c..982b0cefb 100644
--- a/testcases/web/verification/04_List_Operations.scala
+++ b/testcases/web/verification/04_List_Operations.scala
@@ -14,12 +14,12 @@ object ListOperations {
case class IP(fst: BigInt, snd: BigInt) extends IntPair
def size(l: List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def iplSize(l: IntPairList) : BigInt = (l match {
- case IPNil => 0
+ case IPNil => BigInt(0)
case IPCons(_, xs) => 1 + iplSize(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/06_Red-Black_Tree.scala b/testcases/web/verification/06_Red-Black_Tree.scala
index 3adc6c8cb..9a9553146 100644
--- a/testcases/web/verification/06_Red-Black_Tree.scala
+++ b/testcases/web/verification/06_Red-Black_Tree.scala
@@ -20,7 +20,7 @@ object RedBlackTree {
}
def size(t: Tree) : BigInt = t match {
- case Empty => 0
+ case Empty => BigInt(0)
case Node(_, l, v, r) => size(l) + 1 + size(r)
}
diff --git a/testcases/web/verification/07_Search_Linked-List.scala b/testcases/web/verification/07_Search_Linked-List.scala
index 16f1c550e..8d743bd21 100644
--- a/testcases/web/verification/07_Search_Linked-List.scala
+++ b/testcases/web/verification/07_Search_Linked-List.scala
@@ -7,7 +7,7 @@ object SearchLinkedList {
case object Nil extends List
def size(list : List) : BigInt = (list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
@@ -17,8 +17,8 @@ object SearchLinkedList {
})
def firstZero(list : List) : BigInt = (list match {
- case Nil => 0
- case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ case Nil => BigInt(0)
+ case Cons(x, xs) => if (x == 0) BigInt(0) else firstZero(xs) + 1
}) ensuring (res =>
res >= 0 && (if (contains(list, 0)) {
firstZeroAtPos(list, res)
diff --git a/testcases/web/verification/08_Sum_and_Max.scala b/testcases/web/verification/08_Sum_and_Max.scala
index 24d279515..9dcc6d333 100644
--- a/testcases/web/verification/08_Sum_and_Max.scala
+++ b/testcases/web/verification/08_Sum_and_Max.scala
@@ -18,12 +18,12 @@ object SumAndMax {
}
def sum(list : List) : BigInt = list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(x, xs) => x + sum(xs)
}
def size(list : List) : BigInt = (list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/14_HeapSort.scala b/testcases/web/verification/14_HeapSort.scala
index 22d9d55f3..4537664e7 100644
--- a/testcases/web/verification/14_HeapSort.scala
+++ b/testcases/web/verification/14_HeapSort.scala
@@ -8,7 +8,7 @@ object HeapSort {
def rightHeight(h: Heap): BigInt = {
h match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, _, _, r) => rightHeight(r) + 1
}
} ensuring (_ >= 0)
@@ -40,7 +40,7 @@ object HeapSort {
def heapSize(t: Heap): BigInt = {
(t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, v, l, r) => heapSize(l) + 1 + heapSize(r)
})
} ensuring (_ >= 0)
diff --git a/testcases/web/verification/15_LeftistHeap.scala b/testcases/web/verification/15_LeftistHeap.scala
index 356af0154..9ab1a583a 100644
--- a/testcases/web/verification/15_LeftistHeap.scala
+++ b/testcases/web/verification/15_LeftistHeap.scala
@@ -8,7 +8,7 @@ object HeapSort {
def rightHeight(h: Heap): BigInt = {
h match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, _, _, r) => rightHeight(r) + 1
}
} ensuring (_ >= 0)
@@ -40,7 +40,7 @@ object HeapSort {
def heapSize(t: Heap): BigInt = {
(t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, v, l, r) => heapSize(l) + 1 + heapSize(r)
})
} ensuring (_ >= 0)
@@ -117,7 +117,7 @@ object HeapSort {
def heapElements(t: Heap): List[BigInt] = {
require(hasLeftistProperty(t))
t match {
- case Leaf() => Nil()
+ case Leaf() => Nil[BigInt]()
case Node(_, v, l, r) =>
v :: append(heapElements(l), heapElements(r))
}
--
GitLab