moving more tests

mytest/Capture.scala

-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:

mytest/Match.scala

-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)
-}

mytest/NAryOp.scala

-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
-
-}

mytest/ValSideEffect.scala

-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:

mytest/WhileTest.scala

-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)
-}

testcases/regression/Nested2.scala

+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: