From 54e1f4ae160a40f753f51b92bcfa04cd5e067e12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Wed, 24 Oct 2012 14:42:18 -0700 Subject: [PATCH] add regression to the top level and adapt run-tests script --- regression/error/Array1.scala | 8 ++++++ regression/error/Array10.scala | 12 +++++++++ regression/error/Array2.scala | 9 +++++++ regression/error/Array3.scala | 12 +++++++++ regression/error/Array4.scala | 8 ++++++ regression/error/Array5.scala | 10 +++++++ regression/error/Array6.scala | 10 +++++++ regression/error/Array7.scala | 9 +++++++ regression/error/Array8.scala | 7 +++++ regression/error/Array9.scala | 11 ++++++++ regression/error/InstanceOf1.scala | 23 ++++++++++++++++ regression/invalid/Array1.scala | 9 +++++++ regression/invalid/Array2.scala | 9 +++++++ regression/invalid/Array3.scala | 16 +++++++++++ regression/invalid/Array4.scala | 9 +++++++ regression/invalid/Array5.scala | 10 +++++++ regression/invalid/Epsilon1.scala | 12 +++++++++ regression/invalid/Epsilon2.scala | 11 ++++++++ regression/invalid/Epsilon3.scala | 9 +++++++ regression/invalid/Epsilon4.scala | 27 +++++++++++++++++++ regression/invalid/Epsilon5.scala | 9 +++++++ regression/invalid/Epsilon6.scala | 9 +++++++ regression/invalid/IfExpr1.scala | 13 +++++++++ regression/invalid/IfExpr2.scala | 14 ++++++++++ regression/invalid/MyTuple1.scala | 11 ++++++++ regression/invalid/MyTuple2.scala | 14 ++++++++++ regression/invalid/MyTuple3.scala | 7 +++++ regression/invalid/Unit1.scala | 7 +++++ regression/valid/Array1.scala | 9 +++++++ regression/valid/Array10.scala | 9 +++++++ regression/valid/Array2.scala | 9 +++++++ regression/valid/Array3.scala | 16 +++++++++++ regression/valid/Array4.scala | 15 +++++++++++ regression/valid/Array5.scala | 20 ++++++++++++++ regression/valid/Array6.scala | 15 +++++++++++ regression/valid/Array7.scala | 17 ++++++++++++ regression/valid/Array8.scala | 8 ++++++ regression/valid/Array9.scala | 15 +++++++++++ regression/valid/Assign1.scala | 12 +++++++++ regression/valid/Epsilon1.scala | 9 +++++++ regression/valid/Epsilon2.scala | 13 +++++++++ regression/valid/Epsilon3.scala | 9 +++++++ regression/valid/Epsilon4.scala | 32 ++++++++++++++++++++++ regression/valid/Epsilon5.scala | 9 +++++++ regression/valid/Field1.scala | 11 ++++++++ regression/valid/Field2.scala | 11 ++++++++ regression/valid/IfExpr1.scala | 13 +++++++++ regression/valid/IfExpr2.scala | 14 ++++++++++ regression/valid/IfExpr3.scala | 19 +++++++++++++ regression/valid/IfExpr4.scala | 18 +++++++++++++ regression/valid/InstanceOf1.scala | 18 +++++++++++++ regression/valid/MyTuple1.scala | 11 ++++++++ regression/valid/MyTuple2.scala | 14 ++++++++++ regression/valid/MyTuple3.scala | 8 ++++++ regression/valid/MyTuple4.scala | 14 ++++++++++ regression/valid/MyTuple5.scala | 16 +++++++++++ regression/valid/MyTuple6.scala | 8 ++++++ regression/valid/Nested1.scala | 15 +++++++++++ regression/valid/Nested10.scala | 14 ++++++++++ regression/valid/Nested11.scala | 14 ++++++++++ regression/valid/Nested12.scala | 17 ++++++++++++ regression/valid/Nested13.scala | 21 +++++++++++++++ regression/valid/Nested14.scala | 11 ++++++++ regression/valid/Nested2.scala | 13 +++++++++ regression/valid/Nested3.scala | 15 +++++++++++ regression/valid/Nested4.scala | 19 +++++++++++++ regression/valid/Nested5.scala | 12 +++++++++ regression/valid/Nested6.scala | 14 ++++++++++ regression/valid/Nested7.scala | 19 +++++++++++++ regression/valid/Nested8.scala | 43 ++++++++++++++++++++++++++++++ regression/valid/Nested9.scala | 23 ++++++++++++++++ regression/valid/NestedVar.scala | 17 ++++++++++++ regression/valid/Unit1.scala | 7 +++++ regression/valid/Unit2.scala | 7 +++++ regression/valid/While1.scala | 13 +++++++++ regression/valid/While2.scala | 13 +++++++++ regression/valid/While3.scala | 13 +++++++++ run-tests.sh | 15 ++++++----- 78 files changed, 1035 insertions(+), 7 deletions(-) create mode 100644 regression/error/Array1.scala create mode 100644 regression/error/Array10.scala create mode 100644 regression/error/Array2.scala create mode 100644 regression/error/Array3.scala create mode 100644 regression/error/Array4.scala create mode 100644 regression/error/Array5.scala create mode 100644 regression/error/Array6.scala create mode 100644 regression/error/Array7.scala create mode 100644 regression/error/Array8.scala create mode 100644 regression/error/Array9.scala create mode 100644 regression/error/InstanceOf1.scala create mode 100644 regression/invalid/Array1.scala create mode 100644 regression/invalid/Array2.scala create mode 100644 regression/invalid/Array3.scala create mode 100644 regression/invalid/Array4.scala create mode 100644 regression/invalid/Array5.scala create mode 100644 regression/invalid/Epsilon1.scala create mode 100644 regression/invalid/Epsilon2.scala create mode 100644 regression/invalid/Epsilon3.scala create mode 100644 regression/invalid/Epsilon4.scala create mode 100644 regression/invalid/Epsilon5.scala create mode 100644 regression/invalid/Epsilon6.scala create mode 100644 regression/invalid/IfExpr1.scala create mode 100644 regression/invalid/IfExpr2.scala create mode 100644 regression/invalid/MyTuple1.scala create mode 100644 regression/invalid/MyTuple2.scala create mode 100644 regression/invalid/MyTuple3.scala create mode 100644 regression/invalid/Unit1.scala create mode 100644 regression/valid/Array1.scala create mode 100644 regression/valid/Array10.scala create mode 100644 regression/valid/Array2.scala create mode 100644 regression/valid/Array3.scala create mode 100644 regression/valid/Array4.scala create mode 100644 regression/valid/Array5.scala create mode 100644 regression/valid/Array6.scala create mode 100644 regression/valid/Array7.scala create mode 100644 regression/valid/Array8.scala create mode 100644 regression/valid/Array9.scala create mode 100644 regression/valid/Assign1.scala create mode 100644 regression/valid/Epsilon1.scala create mode 100644 regression/valid/Epsilon2.scala create mode 100644 regression/valid/Epsilon3.scala create mode 100644 regression/valid/Epsilon4.scala create mode 100644 regression/valid/Epsilon5.scala create mode 100644 regression/valid/Field1.scala create mode 100644 regression/valid/Field2.scala create mode 100644 regression/valid/IfExpr1.scala create mode 100644 regression/valid/IfExpr2.scala create mode 100644 regression/valid/IfExpr3.scala create mode 100644 regression/valid/IfExpr4.scala create mode 100644 regression/valid/InstanceOf1.scala create mode 100644 regression/valid/MyTuple1.scala create mode 100644 regression/valid/MyTuple2.scala create mode 100644 regression/valid/MyTuple3.scala create mode 100644 regression/valid/MyTuple4.scala create mode 100644 regression/valid/MyTuple5.scala create mode 100644 regression/valid/MyTuple6.scala create mode 100644 regression/valid/Nested1.scala create mode 100644 regression/valid/Nested10.scala create mode 100644 regression/valid/Nested11.scala create mode 100644 regression/valid/Nested12.scala create mode 100644 regression/valid/Nested13.scala create mode 100644 regression/valid/Nested14.scala create mode 100644 regression/valid/Nested2.scala create mode 100644 regression/valid/Nested3.scala create mode 100644 regression/valid/Nested4.scala create mode 100644 regression/valid/Nested5.scala create mode 100644 regression/valid/Nested6.scala create mode 100644 regression/valid/Nested7.scala create mode 100644 regression/valid/Nested8.scala create mode 100644 regression/valid/Nested9.scala create mode 100644 regression/valid/NestedVar.scala create mode 100644 regression/valid/Unit1.scala create mode 100644 regression/valid/Unit2.scala create mode 100644 regression/valid/While1.scala create mode 100644 regression/valid/While2.scala create mode 100644 regression/valid/While3.scala diff --git a/regression/error/Array1.scala b/regression/error/Array1.scala new file mode 100644 index 000000000..d0056f188 --- /dev/null +++ b/regression/error/Array1.scala @@ -0,0 +1,8 @@ +object Array1 { + + def foo(): Int = { + (Array.fill(5)(5))(2) = 3 + 0 + } + +} diff --git a/regression/error/Array10.scala b/regression/error/Array10.scala new file mode 100644 index 000000000..9973626b8 --- /dev/null +++ b/regression/error/Array10.scala @@ -0,0 +1,12 @@ +object Array10 { + + def foo(): Int = { + val a = Array.fill(5)(0) + def rec(): Array[Int] = { + a + } + val b = rec() + b(0) + } + +} diff --git a/regression/error/Array2.scala b/regression/error/Array2.scala new file mode 100644 index 000000000..9154460c3 --- /dev/null +++ b/regression/error/Array2.scala @@ -0,0 +1,9 @@ +object Array2 { + + def foo(): Int = { + val a = Array.fill(5)(5) + val b = a + b(3) + } + +} diff --git a/regression/error/Array3.scala b/regression/error/Array3.scala new file mode 100644 index 000000000..a2c2fbd6d --- /dev/null +++ b/regression/error/Array3.scala @@ -0,0 +1,12 @@ +object Array3 { + + def foo(): Int = { + val a = Array.fill(5)(5) + if(a.length > 2) + a(1) = 2 + else + 0 + 0 + } + +} diff --git a/regression/error/Array4.scala b/regression/error/Array4.scala new file mode 100644 index 000000000..5ab0115af --- /dev/null +++ b/regression/error/Array4.scala @@ -0,0 +1,8 @@ +object Array4 { + + def foo(a: Array[Int]): Int = { + val b = a + b(3) + } + +} diff --git a/regression/error/Array5.scala b/regression/error/Array5.scala new file mode 100644 index 000000000..005d3d389 --- /dev/null +++ b/regression/error/Array5.scala @@ -0,0 +1,10 @@ +object Array5 { + + def foo(a: Array[Int]): Int = { + a(2) = 4 + a(2) + } + +} + +// vim: set ts=4 sw=4 et: diff --git a/regression/error/Array6.scala b/regression/error/Array6.scala new file mode 100644 index 000000000..15c87a085 --- /dev/null +++ b/regression/error/Array6.scala @@ -0,0 +1,10 @@ + +object Array6 { + + def foo(): Int = { + val a = Array.fill(5)(5) + var b = a + b(0) + } + +} diff --git a/regression/error/Array7.scala b/regression/error/Array7.scala new file mode 100644 index 000000000..abb83e1c0 --- /dev/null +++ b/regression/error/Array7.scala @@ -0,0 +1,9 @@ +object Array7 { + + def foo(): Int = { + val a = Array.fill(5)(5) + var b = a + b(0) + } + +} diff --git a/regression/error/Array8.scala b/regression/error/Array8.scala new file mode 100644 index 000000000..89af32efd --- /dev/null +++ b/regression/error/Array8.scala @@ -0,0 +1,7 @@ +object Array8 { + + def foo(a: Array[Int]): Array[Int] = { + a + } + +} diff --git a/regression/error/Array9.scala b/regression/error/Array9.scala new file mode 100644 index 000000000..5dc9d3aea --- /dev/null +++ b/regression/error/Array9.scala @@ -0,0 +1,11 @@ +object Array9 { + + def foo(a: Array[Int]): Int = { + def rec(): Array[Int] = { + a + } + val b = rec() + b(0) + } + +} diff --git a/regression/error/InstanceOf1.scala b/regression/error/InstanceOf1.scala new file mode 100644 index 000000000..a1974b4bc --- /dev/null +++ b/regression/error/InstanceOf1.scala @@ -0,0 +1,23 @@ +object InstanceOf1 { + + abstract class A + case class B(i: Int) extends A + case class C(i: Int) extends A + + abstract class Z + case class Y(i: Int) extends Z + + def foo(): Int = { + //require(3.isInstanceOf[Int]) + val b: A = B(2) + if(b.isInstanceOf[Y]) + 0 + else + -1 + } ensuring(_ == 0) + + def bar(): Int = foo() + +} + +// vim: set ts=4 sw=4 et: diff --git a/regression/invalid/Array1.scala b/regression/invalid/Array1.scala new file mode 100644 index 000000000..a8451250c --- /dev/null +++ b/regression/invalid/Array1.scala @@ -0,0 +1,9 @@ +object Array1 { + + def foo(): Int = { + val a = Array.fill(5)(0) + a(2) = 3 + a(2) + } ensuring(_ == 0) + +} diff --git a/regression/invalid/Array2.scala b/regression/invalid/Array2.scala new file mode 100644 index 000000000..54ab5e3c2 --- /dev/null +++ b/regression/invalid/Array2.scala @@ -0,0 +1,9 @@ +object Array2 { + + def foo(): Int = { + val a = Array.fill(5)(0) + a(2) = 3 + a.length + } ensuring(_ == 4) + +} diff --git a/regression/invalid/Array3.scala b/regression/invalid/Array3.scala new file mode 100644 index 000000000..0c1bb76fd --- /dev/null +++ b/regression/invalid/Array3.scala @@ -0,0 +1,16 @@ +import leon.Utils._ + +object Array3 { + + def foo(): Int = { + val a = Array.fill(5)(3) + var i = 0 + var sum = 0 + (while(i <= a.length) { + sum = sum + a(i) + i = i + 1 + }) invariant(i >= 0) + sum + } ensuring(_ == 15) + +} diff --git a/regression/invalid/Array4.scala b/regression/invalid/Array4.scala new file mode 100644 index 000000000..5b5e74061 --- /dev/null +++ b/regression/invalid/Array4.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Array4 { + + def foo(a: Array[Int]): Int = { + a(2) + } + +} diff --git a/regression/invalid/Array5.scala b/regression/invalid/Array5.scala new file mode 100644 index 000000000..ecb003349 --- /dev/null +++ b/regression/invalid/Array5.scala @@ -0,0 +1,10 @@ +import leon.Utils._ + +object Array4 { + + def foo(a: Array[Int]): Int = { + require(a.length > 2) + a(2) + } ensuring(_ == 0) + +} diff --git a/regression/invalid/Epsilon1.scala b/regression/invalid/Epsilon1.scala new file mode 100644 index 000000000..c3c0a48be --- /dev/null +++ b/regression/invalid/Epsilon1.scala @@ -0,0 +1,12 @@ +import leon.Utils._ + +object Epsilon1 { + + def rand2(x: Int): Int = epsilon((y: Int) => true) + + //this should not hold + def property2(x: Int): Boolean = { + rand2(x) == rand2(x+1) + } holds + +} diff --git a/regression/invalid/Epsilon2.scala b/regression/invalid/Epsilon2.scala new file mode 100644 index 000000000..20699fc42 --- /dev/null +++ b/regression/invalid/Epsilon2.scala @@ -0,0 +1,11 @@ +import leon.Utils._ + +object Epsilon1 { + + def rand3(x: Int): Int = epsilon((y: Int) => x == x) + + //this should not hold + def property3(x: Int): Boolean = { + rand3(x) == rand3(x+1) + } holds +} diff --git a/regression/invalid/Epsilon3.scala b/regression/invalid/Epsilon3.scala new file mode 100644 index 000000000..5ff47b6d6 --- /dev/null +++ b/regression/invalid/Epsilon3.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Epsilon3 { + + def posWrong(): Int = { + epsilon((y: Int) => y >= 0) + } ensuring(_ > 0) + +} diff --git a/regression/invalid/Epsilon4.scala b/regression/invalid/Epsilon4.scala new file mode 100644 index 000000000..6619e59d6 --- /dev/null +++ b/regression/invalid/Epsilon4.scala @@ -0,0 +1,27 @@ +import leon.Utils._ + +object Epsilon4 { + + sealed abstract class MyList + case class MyCons(head: Int, tail: MyList) extends MyList + case class MyNil() extends MyList + + def size(lst: MyList): Int = (lst match { + case MyNil() => 0 + case MyCons(_, xs) => 1 + size(xs) + }) + + def toSet(lst: MyList): Set[Int] = lst match { + case MyCons(x, xs) => toSet(xs) ++ Set(x) + case MyNil() => Set[Int]() + } + + def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else { + val elem = epsilon((x : Int) => set contains x) + MyCons(elem, toList(set -- Set[Int](elem))) + } + + + def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds + //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds +} diff --git a/regression/invalid/Epsilon5.scala b/regression/invalid/Epsilon5.scala new file mode 100644 index 000000000..b96fa7564 --- /dev/null +++ b/regression/invalid/Epsilon5.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Epsilon5 { + + def fooWrong(x: Int, y: Int): Int = { + epsilon((z: Int) => z >= x && z <= y) + } ensuring(_ > x) + +} diff --git a/regression/invalid/Epsilon6.scala b/regression/invalid/Epsilon6.scala new file mode 100644 index 000000000..bc5aca78c --- /dev/null +++ b/regression/invalid/Epsilon6.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Epsilon6 { + + def greaterWrong(x: Int): Int = { + epsilon((y: Int) => y >= x) + } ensuring(_ > x) + +} diff --git a/regression/invalid/IfExpr1.scala b/regression/invalid/IfExpr1.scala new file mode 100644 index 000000000..25ae2a210 --- /dev/null +++ b/regression/invalid/IfExpr1.scala @@ -0,0 +1,13 @@ +object IfExpr1 { + + def foo(): Int = { + var a = 1 + var b = 2 + if({a = a + 1; a != b}) + a = a + 3 + else + b = a + b + a + } ensuring(_ == 3) + +} diff --git a/regression/invalid/IfExpr2.scala b/regression/invalid/IfExpr2.scala new file mode 100644 index 000000000..1284904b5 --- /dev/null +++ b/regression/invalid/IfExpr2.scala @@ -0,0 +1,14 @@ +object IfExpr2 { + + def foo(): Int = { + var a = 1 + var b = 2 + if(a < b) { + a = a + 3 + b = b + 2 + a = a + b + } + a + } ensuring(_ == 0) + +} diff --git a/regression/invalid/MyTuple1.scala b/regression/invalid/MyTuple1.scala new file mode 100644 index 000000000..f2b06b5b2 --- /dev/null +++ b/regression/invalid/MyTuple1.scala @@ -0,0 +1,11 @@ +object MyTuple1 { + + def foo(): Int = { + val t = (1, true, 3) + val a1 = t._1 + val a2 = t._2 + val a3 = t._3 + a3 + } ensuring( _ == 1) + +} diff --git a/regression/invalid/MyTuple2.scala b/regression/invalid/MyTuple2.scala new file mode 100644 index 000000000..22b62dc75 --- /dev/null +++ b/regression/invalid/MyTuple2.scala @@ -0,0 +1,14 @@ +object MyTuple2 { + + abstract class A + case class B(i: Int) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t = (B(2), C(B(3))) + t match { + case (B(x), C(y)) => x + } + } ensuring( _ == 3) + +} diff --git a/regression/invalid/MyTuple3.scala b/regression/invalid/MyTuple3.scala new file mode 100644 index 000000000..da9f85b16 --- /dev/null +++ b/regression/invalid/MyTuple3.scala @@ -0,0 +1,7 @@ +object MyTuple3 { + + def foo(t: (Int, Int)): (Int, Int) = { + t + } ensuring(res => res._1 > 0 && res._2 > 1) + +} diff --git a/regression/invalid/Unit1.scala b/regression/invalid/Unit1.scala new file mode 100644 index 000000000..789a8f058 --- /dev/null +++ b/regression/invalid/Unit1.scala @@ -0,0 +1,7 @@ +object Unit1 { + + def foo(u: Unit): Unit = ({ + u + }) ensuring(_ != ()) + +} diff --git a/regression/valid/Array1.scala b/regression/valid/Array1.scala new file mode 100644 index 000000000..3815f0344 --- /dev/null +++ b/regression/valid/Array1.scala @@ -0,0 +1,9 @@ +object Array1 { + + def foo(): Int = { + val a = Array.fill(5)(0) + a(2) = 3 + a(2) + } ensuring(_ == 3) + +} diff --git a/regression/valid/Array10.scala b/regression/valid/Array10.scala new file mode 100644 index 000000000..ebb60ad6e --- /dev/null +++ b/regression/valid/Array10.scala @@ -0,0 +1,9 @@ +object Array10 { + + def foo(a: Array[Int]): Int = { + require(a.length > 0) + val b = a.clone + b(0) + } ensuring(res => res == a(0)) + +} diff --git a/regression/valid/Array2.scala b/regression/valid/Array2.scala new file mode 100644 index 000000000..4f149a930 --- /dev/null +++ b/regression/valid/Array2.scala @@ -0,0 +1,9 @@ +object Array2 { + + def foo(): Int = { + val a = Array.fill(5)(0) + a(2) = 3 + a.length + } ensuring(_ == 5) + +} diff --git a/regression/valid/Array3.scala b/regression/valid/Array3.scala new file mode 100644 index 000000000..bbb1845b8 --- /dev/null +++ b/regression/valid/Array3.scala @@ -0,0 +1,16 @@ +import leon.Utils._ + +object Array3 { + + def foo(): Int = { + val a = Array.fill(5)(3) + var i = 0 + var sum = 0 + (while(i < a.length) { + sum = sum + a(i) + i = i + 1 + }) invariant(i >= 0) + sum + } ensuring(_ == 15) + +} diff --git a/regression/valid/Array4.scala b/regression/valid/Array4.scala new file mode 100644 index 000000000..fd76e02fa --- /dev/null +++ b/regression/valid/Array4.scala @@ -0,0 +1,15 @@ +import leon.Utils._ + +object Array4 { + + def foo(a: Array[Int]): Int = { + var i = 0 + var sum = 0 + (while(i < a.length) { + sum = sum + a(i) + i = i + 1 + }) invariant(i >= 0) + sum + } + +} diff --git a/regression/valid/Array5.scala b/regression/valid/Array5.scala new file mode 100644 index 000000000..14bed6eff --- /dev/null +++ b/regression/valid/Array5.scala @@ -0,0 +1,20 @@ +import leon.Utils._ + +object Array5 { + + def foo(a: Array[Int]): Int = { + var i = 0 + var sum = 0 + (while(i < a.length) { + sum = sum + a(i) + i = i + 1 + }) invariant(i >= 0) + sum + } + + def bar(): Int = { + val a = Array.fill(5)(5) + foo(a) + } + +} diff --git a/regression/valid/Array6.scala b/regression/valid/Array6.scala new file mode 100644 index 000000000..bdd6b0c5d --- /dev/null +++ b/regression/valid/Array6.scala @@ -0,0 +1,15 @@ +import leon.Utils._ + +object Array6 { + + def foo(a: Array[Int]): Int = { + require(a.length > 2 && a(2) == 5) + a(2) + } ensuring(_ == 5) + + def bar(): Int = { + val a = Array.fill(5)(5) + foo(a) + } + +} diff --git a/regression/valid/Array7.scala b/regression/valid/Array7.scala new file mode 100644 index 000000000..55bbbb729 --- /dev/null +++ b/regression/valid/Array7.scala @@ -0,0 +1,17 @@ +import leon.Utils._ + +object Array7 { + + def foo(a: Array[Int]): Array[Int] = { + require(a.length > 0) + val a2 = Array.fill(a.length)(0) + var i = 0 + (while(i < a.length) { + a2(i) = a(i) + i = i + 1 + }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true)) + a2 + } ensuring(_(0) == a(0)) + + +} diff --git a/regression/valid/Array8.scala b/regression/valid/Array8.scala new file mode 100644 index 000000000..270b18122 --- /dev/null +++ b/regression/valid/Array8.scala @@ -0,0 +1,8 @@ +object Array8 { + + def foo(a: Array[Int]): Array[Int] = { + require(a.length >= 2) + a.updated(1, 3) + } ensuring(res => res.length == a.length && res(1) == 3) + +} diff --git a/regression/valid/Array9.scala b/regression/valid/Array9.scala new file mode 100644 index 000000000..f49333236 --- /dev/null +++ b/regression/valid/Array9.scala @@ -0,0 +1,15 @@ +object Array9 { + + def foo(i: Int): Array[Int] = { + require(i > 0) + val a = Array.fill(i)(0) + a + } ensuring(res => res.length == i) + + def bar(i: Int): Int = { + require(i > 0) + val b = foo(i) + b(0) + } + +} diff --git a/regression/valid/Assign1.scala b/regression/valid/Assign1.scala new file mode 100644 index 000000000..0506c6afb --- /dev/null +++ b/regression/valid/Assign1.scala @@ -0,0 +1,12 @@ +object Assign1 { + + def foo(): Int = { + var a = 0 + val tmp = a + 1 + a = a + 2 + a = a + tmp + a = a + 4 + a + } ensuring(_ == 7) + +} diff --git a/regression/valid/Epsilon1.scala b/regression/valid/Epsilon1.scala new file mode 100644 index 000000000..2ae7201dd --- /dev/null +++ b/regression/valid/Epsilon1.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Epsilon1 { + + def greater(x: Int): Int = { + epsilon((y: Int) => y > x) + } ensuring(_ >= x) + +} diff --git a/regression/valid/Epsilon2.scala b/regression/valid/Epsilon2.scala new file mode 100644 index 000000000..36e5268e2 --- /dev/null +++ b/regression/valid/Epsilon2.scala @@ -0,0 +1,13 @@ +import leon.Utils._ + +object Epsilon1 { + + def rand(): Int = epsilon((x: Int) => true) + + //this should hold, that is the expected semantic of our epsilon + def property1(): Boolean = { + rand() == rand() + } holds + + +} diff --git a/regression/valid/Epsilon3.scala b/regression/valid/Epsilon3.scala new file mode 100644 index 000000000..f652016d2 --- /dev/null +++ b/regression/valid/Epsilon3.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Epsilon3 { + + def pos(): Int = { + epsilon((y: Int) => y > 0) + } ensuring(_ >= 0) + +} diff --git a/regression/valid/Epsilon4.scala b/regression/valid/Epsilon4.scala new file mode 100644 index 000000000..174042863 --- /dev/null +++ b/regression/valid/Epsilon4.scala @@ -0,0 +1,32 @@ +import leon.Utils._ + +object Epsilon4 { + + sealed abstract class MyList + case class MyCons(head: Int, tail: MyList) extends MyList + case class MyNil() extends MyList + + def size(lst: MyList): Int = (lst match { + case MyNil() => 0 + case MyCons(_, xs) => 1 + size(xs) + }) + + def toSet(lst: MyList): Set[Int] = lst match { + case MyCons(x, xs) => toSet(xs) ++ Set(x) + case MyNil() => Set[Int]() + } + + def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else { + val elem = epsilon((x : Int) => set contains x) + MyCons(elem, toList(set -- Set[Int](elem))) + } + + //timeout, but this probably means that it is valid as expected + //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds + + def propertyBase(lst: MyList): Boolean = ({ + require(lst match { case MyNil() => true case _ => false}) + size(toList(toSet(lst))) <= size(lst) + }) holds + +} diff --git a/regression/valid/Epsilon5.scala b/regression/valid/Epsilon5.scala new file mode 100644 index 000000000..0427cf086 --- /dev/null +++ b/regression/valid/Epsilon5.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Epsilon5 { + + def foo(x: Int, y: Int): Int = { + epsilon((z: Int) => z > x && z < y) + } ensuring(_ >= x) + +} diff --git a/regression/valid/Field1.scala b/regression/valid/Field1.scala new file mode 100644 index 000000000..116557ab7 --- /dev/null +++ b/regression/valid/Field1.scala @@ -0,0 +1,11 @@ +object Field1 { + + abstract sealed class A + case class B(size: Int) extends A + + def foo(): Int = { + val b = B(3) + b.size + } ensuring(_ == 3) + +} diff --git a/regression/valid/Field2.scala b/regression/valid/Field2.scala new file mode 100644 index 000000000..9a9661023 --- /dev/null +++ b/regression/valid/Field2.scala @@ -0,0 +1,11 @@ +object Field2 { + + abstract sealed class A + case class B(length: Int) extends A + + def foo(): Int = { + val b = B(3) + b.length + } ensuring(_ == 3) + +} diff --git a/regression/valid/IfExpr1.scala b/regression/valid/IfExpr1.scala new file mode 100644 index 000000000..82db13d52 --- /dev/null +++ b/regression/valid/IfExpr1.scala @@ -0,0 +1,13 @@ +object IfExpr1 { + + def foo(): Int = { + var a = 1 + var b = 2 + if({a = a + 1; a != b}) + a = a + 3 + else + b = a + b + a + } ensuring(_ == 2) + +} diff --git a/regression/valid/IfExpr2.scala b/regression/valid/IfExpr2.scala new file mode 100644 index 000000000..7a681bc72 --- /dev/null +++ b/regression/valid/IfExpr2.scala @@ -0,0 +1,14 @@ +object IfExpr2 { + + def foo(): Int = { + var a = 1 + var b = 2 + if(a < b) { + a = a + 3 + b = b + 2 + a = a + b + } + a + } ensuring(_ == 8) + +} diff --git a/regression/valid/IfExpr3.scala b/regression/valid/IfExpr3.scala new file mode 100644 index 000000000..86d4e494a --- /dev/null +++ b/regression/valid/IfExpr3.scala @@ -0,0 +1,19 @@ +object IfExpr1 { + + def foo(a: Int): Int = { + + if(a > 0) { + var a = 1 + var b = 2 + a = 3 + a + b + } else { + 5 + //var a = 3 + //var b = 1 + //b = b + 1 + //a + b + } + } ensuring(_ == 5) + +} diff --git a/regression/valid/IfExpr4.scala b/regression/valid/IfExpr4.scala new file mode 100644 index 000000000..94b99fde3 --- /dev/null +++ b/regression/valid/IfExpr4.scala @@ -0,0 +1,18 @@ +object IfExpr4 { + + def foo(a: Int): Int = { + + if(a > 0) { + var a = 1 + var b = 2 + a = 3 + a + b + } else { + var a = 3 + var b = 1 + b = b + 1 + a + b + } + } ensuring(_ == 5) + +} diff --git a/regression/valid/InstanceOf1.scala b/regression/valid/InstanceOf1.scala new file mode 100644 index 000000000..1c52338bb --- /dev/null +++ b/regression/valid/InstanceOf1.scala @@ -0,0 +1,18 @@ +object InstanceOf1 { + + abstract class A + case class B(i: Int) extends A + case class C(i: Int) extends A + + def foo(): Int = { + require(C(3).isInstanceOf[C]) + val b: A = B(2) + if(b.isInstanceOf[B]) + 0 + else + -1 + } ensuring(_ == 0) + + def bar(): Int = foo() + +} diff --git a/regression/valid/MyTuple1.scala b/regression/valid/MyTuple1.scala new file mode 100644 index 000000000..48383898e --- /dev/null +++ b/regression/valid/MyTuple1.scala @@ -0,0 +1,11 @@ +object MyTuple1 { + + def foo(): Int = { + val t = (1, true, 3) + val a1 = t._1 + val a2 = t._2 + val a3 = t._3 + a3 + } ensuring( _ == 3) + +} diff --git a/regression/valid/MyTuple2.scala b/regression/valid/MyTuple2.scala new file mode 100644 index 000000000..9fd21eb20 --- /dev/null +++ b/regression/valid/MyTuple2.scala @@ -0,0 +1,14 @@ +object MyTuple2 { + + abstract class A + case class B(i: Int) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t = (B(2), C(B(3))) + t match { + case (B(x), C(y)) => x + } + } ensuring(_ == 2) + +} diff --git a/regression/valid/MyTuple3.scala b/regression/valid/MyTuple3.scala new file mode 100644 index 000000000..2e14c067b --- /dev/null +++ b/regression/valid/MyTuple3.scala @@ -0,0 +1,8 @@ +object MyTuple3 { + + def foo(): Int = { + val t = ((2, 3), true) + t._1._2 + } ensuring( _ == 3) + +} diff --git a/regression/valid/MyTuple4.scala b/regression/valid/MyTuple4.scala new file mode 100644 index 000000000..6fcfed661 --- /dev/null +++ b/regression/valid/MyTuple4.scala @@ -0,0 +1,14 @@ + +object MyTuple4 { + + abstract class A + case class B(i: Int) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t = (1, (C(B(4)), 2), 3) + val (a1, (C(B(x)), a2), a3) = t + x + } ensuring( _ == 4) + +} diff --git a/regression/valid/MyTuple5.scala b/regression/valid/MyTuple5.scala new file mode 100644 index 000000000..6a55bc8c9 --- /dev/null +++ b/regression/valid/MyTuple5.scala @@ -0,0 +1,16 @@ +object MyTuple1 { + + abstract class A + case class B(t: (Int, Int)) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3) + t match { + case (_, (B((x, y)), _), _) => x + case (_, (C(B((_, x))), _), y) => x + case (_, _, x) => x + } + } ensuring( _ == 5) + +} diff --git a/regression/valid/MyTuple6.scala b/regression/valid/MyTuple6.scala new file mode 100644 index 000000000..a54710fbb --- /dev/null +++ b/regression/valid/MyTuple6.scala @@ -0,0 +1,8 @@ +object MyTuple6 { + + def foo(t: (Int, Int)): (Int, Int) = { + require(t._1 > 0 && t._2 > 1) + t + } ensuring(res => res._1 > 0 && res._2 > 1) + +} diff --git a/regression/valid/Nested1.scala b/regression/valid/Nested1.scala new file mode 100644 index 000000000..7745f794f --- /dev/null +++ b/regression/valid/Nested1.scala @@ -0,0 +1,15 @@ +object Nested1 { + + def foo(i: Int): Int = { + val n = 2 + def rec1(j: Int) = i + j + n + def rec2(j: Int) = { + def rec3(k: Int) = k + j + i + rec3(5) + } + rec2(2) + } ensuring(i + 7 == _) + +} + +// vim: set ts=4 sw=4 et: diff --git a/regression/valid/Nested10.scala b/regression/valid/Nested10.scala new file mode 100644 index 000000000..b3c4f8653 --- /dev/null +++ b/regression/valid/Nested10.scala @@ -0,0 +1,14 @@ +object Nested10 { + + def foo(i: Int): Int = { + val n = 2 + def rec1(j: Int) = { + i + j + n + } + def rec2(j: Int) = { + rec1(j) + } + rec2(2) + } ensuring(i + 4 == _) + +} diff --git a/regression/valid/Nested11.scala b/regression/valid/Nested11.scala new file mode 100644 index 000000000..0316fc5f2 --- /dev/null +++ b/regression/valid/Nested11.scala @@ -0,0 +1,14 @@ +object Nested11 { + + abstract class A + case class B(b: Int) extends A + + def foo(i: Int): Int = { + val b: A = B(3) + def rec1(j: Int) = b match { + case B(b) => i + j + b + } + rec1(2) + } ensuring(i + 5 == _) + +} diff --git a/regression/valid/Nested12.scala b/regression/valid/Nested12.scala new file mode 100644 index 000000000..05ac1569f --- /dev/null +++ b/regression/valid/Nested12.scala @@ -0,0 +1,17 @@ +object Nested12 { + + abstract class A + case class B(b: Int) extends A + + def foo(i: Int): Int = { + val b: A = B(3) + def rec1(a: A, j: Int, j2: Int) = a match { + case B(b) => i + j + j2 + b + } + def rec2(a: A, k: Int) = a match { + case B(b) => rec1(a, b, k) + } + rec2(b, 2) + } ensuring(i + 8 == _) + +} diff --git a/regression/valid/Nested13.scala b/regression/valid/Nested13.scala new file mode 100644 index 000000000..ccb742494 --- /dev/null +++ b/regression/valid/Nested13.scala @@ -0,0 +1,21 @@ +object Nested13 { + + abstract class D + case class E(e: Int) extends D + case class F(d: D, f: Int) extends D + + def foo(a : Int): Int = { + + def rec1(d: D, j: Int): Int = d match { + case E(e) => j + e + a + case F(dNext, f) => f + rec1(dNext, j) + } + + def rec2(d: D, i : Int) : Int = d match { + case E(e) => e + case F(dNext, f) => rec1(d, i) + } + + rec2(F(E(2), 3), 0) + } ensuring(a + 5 == _) +} diff --git a/regression/valid/Nested14.scala b/regression/valid/Nested14.scala new file mode 100644 index 000000000..9a79a4f6e --- /dev/null +++ b/regression/valid/Nested14.scala @@ -0,0 +1,11 @@ +object Nested14 { + + def foo(i: Int): Int = { + def rec1(j: Int): Int = { + def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1) + rec2(j) + } + rec1(3) + } ensuring(0 == _) + +} diff --git a/regression/valid/Nested2.scala b/regression/valid/Nested2.scala new file mode 100644 index 000000000..cc7220b02 --- /dev/null +++ b/regression/valid/Nested2.scala @@ -0,0 +1,13 @@ +object Nested2 { + + def foo(a: Int): Int = { + require(a >= 0) + val b = a + 2 + def rec1(c: Int): Int = { + require(c >= 0) + b + c + } + rec1(2) + } ensuring(_ > 0) + +} diff --git a/regression/valid/Nested3.scala b/regression/valid/Nested3.scala new file mode 100644 index 000000000..be6e6d04a --- /dev/null +++ b/regression/valid/Nested3.scala @@ -0,0 +1,15 @@ +object Nested3 { + + def foo(a: Int): Int = { + require(a >= 0 && a <= 50) + val b = a + 2 + val c = a + b + def rec1(d: Int): Int = { + require(d >= 0 && d <= 50) + val e = d + b + c + e + } + rec1(2) + } ensuring(_ > 0) + +} diff --git a/regression/valid/Nested4.scala b/regression/valid/Nested4.scala new file mode 100644 index 000000000..ea1e6066c --- /dev/null +++ b/regression/valid/Nested4.scala @@ -0,0 +1,19 @@ +object Nested4 { + + def foo(a: Int, a2: Int): Int = { + require(a >= 0 && a <= 50) + val b = a + 2 + val c = a + b + if(a2 > a) { + def rec1(d: Int): Int = { + require(d >= 0 && d <= 50) + val e = d + b + c + a2 + e + } ensuring(_ > 0) + rec1(2) + } else { + 5 + } + } ensuring(_ > 0) + +} diff --git a/regression/valid/Nested5.scala b/regression/valid/Nested5.scala new file mode 100644 index 000000000..6ba128f41 --- /dev/null +++ b/regression/valid/Nested5.scala @@ -0,0 +1,12 @@ +object Nested5 { + + def foo(a: Int): Int = { + require(a >= 0) + def bar(b: Int): Int = { + require(b > 0) + b + 3 + } ensuring(a >= 0 && _ == b + 3) + bar(2) + } ensuring(a >= 0 && _ == 5) + +} diff --git a/regression/valid/Nested6.scala b/regression/valid/Nested6.scala new file mode 100644 index 000000000..1c0220c04 --- /dev/null +++ b/regression/valid/Nested6.scala @@ -0,0 +1,14 @@ +object Nested5 { + + def foo(a: Int): Int = { + require(a >= 0) + def bar(b: Int): Int = { + require(b > 0) + b + 3 + } ensuring(prop(a, b) && a >= 0 && _ == b + 3) + bar(2) + } ensuring(a >= 0 && _ == 5) + + def prop(x: Int, y: Int): Boolean = x + y > 0 + +} diff --git a/regression/valid/Nested7.scala b/regression/valid/Nested7.scala new file mode 100644 index 000000000..62f5a567f --- /dev/null +++ b/regression/valid/Nested7.scala @@ -0,0 +1,19 @@ +object Nested2 { + + def foo(a: Int): Int = { + require(a >= 0) + val b = a + 2 + def rec1(c: Int): Int = { + require(c >= 0) + b + c + bar(a) + bar(b) + bar(c) + } + rec1(2) + bar(a) + } ensuring(_ > 0) + + + def bar(x: Int): Int = { + require(x >= 0) + x + } ensuring(_ >= 0) + +} diff --git a/regression/valid/Nested8.scala b/regression/valid/Nested8.scala new file mode 100644 index 000000000..e8a05e40e --- /dev/null +++ b/regression/valid/Nested8.scala @@ -0,0 +1,43 @@ +import leon.Utils._ + +object Nested8 { + + def foo(a: Int): Int = { + require(a > 0) + + def bar(b: Int): Int = { + if(a < b) { + def rec(c: Int): Int = { + require(c > 0) + c + b + } ensuring(_ > 0) + rec(2) + } else 3 + } + bar(1) + } ensuring(_ > 0) + + /* + def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = { + require(l1 >= 0 && u1 < l2 && u2 < size) + if(l2 > u2 || l1 > u1) + true + else { + var i = l1 + var j = l2 + var isPartitionned = true + (while(i <= u1) { + j = l2 + (while(j <= u2) { + if(a(i) > a(j)) + isPartitionned = false + j = j + 1 + }) invariant(j >= l2 && i <= u1) + i = i + 1 + }) invariant(i >= l1) + isPartitionned + } + } + */ + +} diff --git a/regression/valid/Nested9.scala b/regression/valid/Nested9.scala new file mode 100644 index 000000000..3344a2c79 --- /dev/null +++ b/regression/valid/Nested9.scala @@ -0,0 +1,23 @@ +object Nested4 { + + def foo(a: Int, a2: Int): Int = { + require(a >= 0 && a <= 50) + val b = a + 2 + val c = a + b + if(a2 > a) { + def rec1(d: Int): Int = { + require(d >= 0 && d <= 50) + val e = d + b + c + a2 + def rec2(f: Int): Int = { + require(f >= c) + f + e + } ensuring(_ > 0) + rec2(c+1) + } ensuring(_ > 0) + rec1(2) + } else { + 5 + } + } ensuring(_ > 0) + +} diff --git a/regression/valid/NestedVar.scala b/regression/valid/NestedVar.scala new file mode 100644 index 000000000..a26b7312b --- /dev/null +++ b/regression/valid/NestedVar.scala @@ -0,0 +1,17 @@ +object NestedVar { + + def foo(): Int = { + val a = 3 + def rec(x: Int): Int = { + var b = 3 + var c = 3 + if(x > 0) + b = 2 + else + c = 2 + c+b + } + rec(a) + } ensuring(_ == 5) + +} diff --git a/regression/valid/Unit1.scala b/regression/valid/Unit1.scala new file mode 100644 index 000000000..a7b890d76 --- /dev/null +++ b/regression/valid/Unit1.scala @@ -0,0 +1,7 @@ +object Unit1 { + + def foo(): Unit = ({ + () + }) ensuring(_ == ()) + +} diff --git a/regression/valid/Unit2.scala b/regression/valid/Unit2.scala new file mode 100644 index 000000000..ac659589a --- /dev/null +++ b/regression/valid/Unit2.scala @@ -0,0 +1,7 @@ +object Unit2 { + + def foo(u: Unit): Unit = { + u + } ensuring(_ == ()) + +} diff --git a/regression/valid/While1.scala b/regression/valid/While1.scala new file mode 100644 index 000000000..0d868b399 --- /dev/null +++ b/regression/valid/While1.scala @@ -0,0 +1,13 @@ +object While1 { + + def foo(): Int = { + var a = 0 + var i = 0 + while(i < 10) { + a = a + 1 + i = i + 1 + } + a + } ensuring(_ == 10) + +} diff --git a/regression/valid/While2.scala b/regression/valid/While2.scala new file mode 100644 index 000000000..e841ed40e --- /dev/null +++ b/regression/valid/While2.scala @@ -0,0 +1,13 @@ +object While1 { + + def foo(): Int = { + var a = 0 + var i = 0 + while(i < 10) { + a = a + i + i = i + 1 + } + a + } ensuring(_ == 45) + +} diff --git a/regression/valid/While3.scala b/regression/valid/While3.scala new file mode 100644 index 000000000..da85d5dfa --- /dev/null +++ b/regression/valid/While3.scala @@ -0,0 +1,13 @@ +object While3 { + + def foo(): Int = { + var a = 0 + var i = 0 + while({i = i+2; i <= 10}) { + a = a + i + i = i - 1 + } + a + } ensuring(_ == 54) + +} diff --git a/run-tests.sh b/run-tests.sh index 1a5be5724..7a36168c1 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -1,36 +1,37 @@ #!/bin/bash -nbtests=$(ls -l testcases/regression/{valid,invalid,error}/*.scala | wc -l) +base=./regression +nbtests=$(ls -l $base/{valid,invalid,error}/*.scala | wc -l) nbsuccess=0 failedtests="" -for f in testcases/regression/valid/*.scala; do +for f in $base/valid/*.scala; do echo -n "Running $f, expecting VALID, got: " res=`./leon --noLuckyTests --timeout=10 --oneline "$f"` echo $res | tr [a-z] [A-Z] - if [ "$res" = valid ]; then + if [ $res = valid ]; then nbsuccess=$((nbsuccess + 1)) else failedtests="$failedtests $f" fi done -for f in testcases/regression/invalid/*.scala; do +for f in $base/invalid/*.scala; do echo -n "Running $f, expecting INVALID, got: " res=`./leon --noLuckyTests --timeout=10 --oneline "$f"` echo $res | tr [a-z] [A-Z] - if [ "$res" = invalid ]; then + if [ $res = invalid ]; then nbsuccess=$((nbsuccess + 1)) else failedtests="$failedtests $f" fi done -for f in testcases/regression/error/*.scala; do +for f in $base/error/*.scala; do echo -n "Running $f, expecting ERROR, got: " res=`./leon --noLuckyTests --timeout=10 --oneline "$f"` echo $res | tr [a-z] [A-Z] - if [ "$res" = error ]; then + if [ $res = error ]; then nbsuccess=$((nbsuccess + 1)) else failedtests="$failedtests $f" -- GitLab