From b59337202f2fbc9d4fd482e6318e7daccab7ad78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Thu, 26 Apr 2012 19:34:14 +0200 Subject: [PATCH] moving more tests --- mytest/Capture.scala | 10 ---------- mytest/Match.scala | 18 ----------------- mytest/NAryOp.scala | 12 ----------- mytest/ValSideEffect.scala | 17 ---------------- mytest/WhileTest.scala | 20 ------------------- {mytest => testcases}/Abs.scala | 0 {mytest => testcases}/BubbleFun.scala | 0 .../BubbleWeakInvariant.scala | 0 {mytest => testcases}/MaxSum.scala | 0 .../regression}/Assign1.scala | 0 .../regression}/IfExpr1.scala | 0 testcases/regression/Nested2.scala | 15 ++++++++++++++ 12 files changed, 15 insertions(+), 77 deletions(-) delete mode 100644 mytest/Capture.scala delete mode 100644 mytest/Match.scala delete mode 100644 mytest/NAryOp.scala delete mode 100644 mytest/ValSideEffect.scala delete mode 100644 mytest/WhileTest.scala rename {mytest => testcases}/Abs.scala (100%) rename {mytest => testcases}/BubbleFun.scala (100%) rename {mytest => testcases}/BubbleWeakInvariant.scala (100%) rename {mytest => testcases}/MaxSum.scala (100%) rename {mytest => testcases/regression}/Assign1.scala (100%) rename {mytest => testcases/regression}/IfExpr1.scala (100%) create mode 100644 testcases/regression/Nested2.scala diff --git a/mytest/Capture.scala b/mytest/Capture.scala deleted file mode 100644 index c1c4c7e1e..000000000 --- a/mytest/Capture.scala +++ /dev/null @@ -1,10 +0,0 @@ -object Capture { - - def foo(i: Int): Int = { - val a = 3 - def rec(j: Int): Int = if(j == a) 0 else 1 - rec(3) - } -} - -// vim: set ts=4 sw=4 et: diff --git a/mytest/Match.scala b/mytest/Match.scala deleted file mode 100644 index 5376cc61d..000000000 --- a/mytest/Match.scala +++ /dev/null @@ -1,18 +0,0 @@ -object Match { - - sealed abstract class A - case class B(b: Int) extends A - case class C(c: Int) extends A - - def foo(a: A): Int = ({ - - var i = 0 - var j = 0 - - {i = i + 1; a} match { - case B(b) => {i = i + 1; b} - case C(c) => {j = j + 1; i = i + 1; c} - } - i - }) ensuring(_ == 2) -} diff --git a/mytest/NAryOp.scala b/mytest/NAryOp.scala deleted file mode 100644 index adf6c84bf..000000000 --- a/mytest/NAryOp.scala +++ /dev/null @@ -1,12 +0,0 @@ -object NAryOp { - - def foo(): Int = ({ - - var a = 2 - bar({a = a + 1; a}, {a = 5 - a; a}, {a = a + 2; a}) - }) ensuring(_ == 9) - - - def bar(i1: Int, i2: Int, i3: Int): Int = i1 + i2 + i3 - -} diff --git a/mytest/ValSideEffect.scala b/mytest/ValSideEffect.scala deleted file mode 100644 index 5beefdaff..000000000 --- a/mytest/ValSideEffect.scala +++ /dev/null @@ -1,17 +0,0 @@ -object ValSideEffect { - - def foo(): Int = ({ - - var a = 2 - var a2 = 1 - - val b = {a = a + 1; a2 = a2 + 1; a} + {a = 5 - a; a} - a = a + 1 - a2 = a2 + 3 - a + a2 + b - }) ensuring(_ == 13) - - -} - -// vim: set ts=4 sw=4 et: diff --git a/mytest/WhileTest.scala b/mytest/WhileTest.scala deleted file mode 100644 index c080552e5..000000000 --- a/mytest/WhileTest.scala +++ /dev/null @@ -1,20 +0,0 @@ -import leon.Utils._ - -object WhileTest { -// object InvariantFunction { -// def invariant(x: Boolean): Unit = () -// } -// implicit def while2Invariant(u: Unit) = InvariantFunction - def foo(x : Int) : Int = { - require(x >= 0) - - var y : Int = x - - (while (y >= 0) { - y = y - 1 - // assert(y >= -1) - }) invariant(y >= -1) - - y + 1 - } ensuring(_ == 0) -} diff --git a/mytest/Abs.scala b/testcases/Abs.scala similarity index 100% rename from mytest/Abs.scala rename to testcases/Abs.scala diff --git a/mytest/BubbleFun.scala b/testcases/BubbleFun.scala similarity index 100% rename from mytest/BubbleFun.scala rename to testcases/BubbleFun.scala diff --git a/mytest/BubbleWeakInvariant.scala b/testcases/BubbleWeakInvariant.scala similarity index 100% rename from mytest/BubbleWeakInvariant.scala rename to testcases/BubbleWeakInvariant.scala diff --git a/mytest/MaxSum.scala b/testcases/MaxSum.scala similarity index 100% rename from mytest/MaxSum.scala rename to testcases/MaxSum.scala diff --git a/mytest/Assign1.scala b/testcases/regression/Assign1.scala similarity index 100% rename from mytest/Assign1.scala rename to testcases/regression/Assign1.scala diff --git a/mytest/IfExpr1.scala b/testcases/regression/IfExpr1.scala similarity index 100% rename from mytest/IfExpr1.scala rename to testcases/regression/IfExpr1.scala diff --git a/testcases/regression/Nested2.scala b/testcases/regression/Nested2.scala new file mode 100644 index 000000000..30830df0b --- /dev/null +++ b/testcases/regression/Nested2.scala @@ -0,0 +1,15 @@ +object Nested2 { + + 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: -- GitLab