From 7a8cfc64fe78cdc7a4166173ac8e779268671ae2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 27 Apr 2012 03:29:16 +0000
Subject: [PATCH] test system

---
 run-tests.sh                                  | 35 +++++++++++++++++++
 .../regression/{ => invalid}/Epsilon1.scala   |  4 ---
 testcases/regression/invalid/Epsilon2.scala   | 11 ++++++
 .../regression/{ => invalid}/Epsilon3.scala   |  4 ---
 .../regression/{ => invalid}/Epsilon4.scala   |  2 --
 .../regression/{ => invalid}/Epsilon5.scala   |  6 ----
 testcases/regression/invalid/MyTuple1.scala   | 11 ++++++
 testcases/regression/invalid/MyTuple2.scala   | 14 ++++++++
 testcases/regression/valid/Epsilon1.scala     |  9 +++++
 .../regression/{ => valid}/Epsilon2.scala     |  5 ---
 testcases/regression/valid/Epsilon3.scala     |  9 +++++
 testcases/regression/valid/Epsilon4.scala     | 32 +++++++++++++++++
 testcases/regression/valid/Epsilon5.scala     |  9 +++++
 .../{MyTuple3.scala => valid/MyTuple1.scala}  |  0
 .../{MyTuple4.scala => valid/MyTuple2.scala}  |  4 +--
 15 files changed, 132 insertions(+), 23 deletions(-)
 create mode 100755 run-tests.sh
 rename testcases/regression/{ => invalid}/Epsilon1.scala (60%)
 create mode 100644 testcases/regression/invalid/Epsilon2.scala
 rename testcases/regression/{ => invalid}/Epsilon3.scala (62%)
 rename testcases/regression/{ => invalid}/Epsilon4.scala (83%)
 rename testcases/regression/{ => invalid}/Epsilon5.scala (53%)
 create mode 100644 testcases/regression/invalid/MyTuple1.scala
 create mode 100644 testcases/regression/invalid/MyTuple2.scala
 create mode 100644 testcases/regression/valid/Epsilon1.scala
 rename testcases/regression/{ => valid}/Epsilon2.scala (72%)
 create mode 100644 testcases/regression/valid/Epsilon3.scala
 create mode 100644 testcases/regression/valid/Epsilon4.scala
 create mode 100644 testcases/regression/valid/Epsilon5.scala
 rename testcases/regression/{MyTuple3.scala => valid/MyTuple1.scala} (100%)
 rename testcases/regression/{MyTuple4.scala => valid/MyTuple2.scala} (82%)

diff --git a/run-tests.sh b/run-tests.sh
new file mode 100755
index 000000000..f1e606a6e
--- /dev/null
+++ b/run-tests.sh
@@ -0,0 +1,35 @@
+#!/bin/sh
+
+nbtests=$(ls -l testcases/regression/*valid/*.scala | wc -l)
+nbsuccess=0
+failedtests=""
+
+for f in testcases/regression/valid/*.scala; do
+  echo -n "Running $f, expecting VALID, got: "
+  res=`./leon --timeout=5 --oneline "$f"`
+  echo $res | tr [a-z] [A-Z]
+  if [ $res = valid ]; then
+    nbsuccess=$((nbsuccess + 1))
+  else
+    failedtests="$failedtests $f"
+  fi
+done
+
+for f in testcases/regression/invalid/*.scala; do
+  echo -n "Running $f, expecting INVALID, got: "
+  res=`./leon --timeout=5 --oneline "$f"`
+  echo $res | tr [a-z] [A-Z]
+  if [ $res = invalid ]; then
+    nbsuccess=$((nbsuccess + 1))
+  else
+    failedtests="$failedtests $f"
+  fi
+done
+
+echo "$nbsuccess out of $nbtests tests were successful"
+if [ $nbtests -eq $nbsuccess ]; then
+  echo "PASSED"
+else
+  echo "ERROR. The following test did not run as expected:"
+  for f in $failedtests; do echo $f; done
+fi
diff --git a/testcases/regression/Epsilon1.scala b/testcases/regression/invalid/Epsilon1.scala
similarity index 60%
rename from testcases/regression/Epsilon1.scala
rename to testcases/regression/invalid/Epsilon1.scala
index 827c1e6e5..859ced1c1 100644
--- a/testcases/regression/Epsilon1.scala
+++ b/testcases/regression/invalid/Epsilon1.scala
@@ -2,10 +2,6 @@ import leon.Utils._
 
 object Epsilon1 {
 
-  def greater(x: Int): Int = {
-    epsilon((y: Int) => y > x)
-  } ensuring(_ >= x)
-
   def greaterWrong(x: Int): Int = {
     epsilon((y: Int) => y >= x)
   } ensuring(_ > x)
diff --git a/testcases/regression/invalid/Epsilon2.scala b/testcases/regression/invalid/Epsilon2.scala
new file mode 100644
index 000000000..20699fc42
--- /dev/null
+++ b/testcases/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/testcases/regression/Epsilon3.scala b/testcases/regression/invalid/Epsilon3.scala
similarity index 62%
rename from testcases/regression/Epsilon3.scala
rename to testcases/regression/invalid/Epsilon3.scala
index 54b73ce93..5ff47b6d6 100644
--- a/testcases/regression/Epsilon3.scala
+++ b/testcases/regression/invalid/Epsilon3.scala
@@ -2,10 +2,6 @@ import leon.Utils._
 
 object Epsilon3 {
 
-  def pos(): Int = {
-    epsilon((y: Int) => y > 0)
-  } ensuring(_ >= 0)
-
   def posWrong(): Int = {
     epsilon((y: Int) => y >= 0)
   } ensuring(_ > 0)
diff --git a/testcases/regression/Epsilon4.scala b/testcases/regression/invalid/Epsilon4.scala
similarity index 83%
rename from testcases/regression/Epsilon4.scala
rename to testcases/regression/invalid/Epsilon4.scala
index ede704be7..52ee6dbe6 100644
--- a/testcases/regression/Epsilon4.scala
+++ b/testcases/regression/invalid/Epsilon4.scala
@@ -21,8 +21,6 @@ object Epsilon4 {
     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 wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
   def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
diff --git a/testcases/regression/Epsilon5.scala b/testcases/regression/invalid/Epsilon5.scala
similarity index 53%
rename from testcases/regression/Epsilon5.scala
rename to testcases/regression/invalid/Epsilon5.scala
index 25d016e1b..b96fa7564 100644
--- a/testcases/regression/Epsilon5.scala
+++ b/testcases/regression/invalid/Epsilon5.scala
@@ -2,14 +2,8 @@ import leon.Utils._
 
 object Epsilon5 {
 
-  def foo(x: Int, y: Int): Int = {
-    epsilon((z: Int) => z > x && z < y)
-  } ensuring(_ >= x)
-
   def fooWrong(x: Int, y: Int): Int = {
     epsilon((z: Int) => z >= x && z <= y)
   } ensuring(_ > x)
 
 }
-
-// vim: set ts=4 sw=4 et:
diff --git a/testcases/regression/invalid/MyTuple1.scala b/testcases/regression/invalid/MyTuple1.scala
new file mode 100644
index 000000000..f2b06b5b2
--- /dev/null
+++ b/testcases/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/testcases/regression/invalid/MyTuple2.scala b/testcases/regression/invalid/MyTuple2.scala
new file mode 100644
index 000000000..22b62dc75
--- /dev/null
+++ b/testcases/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/testcases/regression/valid/Epsilon1.scala b/testcases/regression/valid/Epsilon1.scala
new file mode 100644
index 000000000..2ae7201dd
--- /dev/null
+++ b/testcases/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/testcases/regression/Epsilon2.scala b/testcases/regression/valid/Epsilon2.scala
similarity index 72%
rename from testcases/regression/Epsilon2.scala
rename to testcases/regression/valid/Epsilon2.scala
index 1bf56bdd7..b4f53f36b 100644
--- a/testcases/regression/Epsilon2.scala
+++ b/testcases/regression/valid/Epsilon2.scala
@@ -4,7 +4,6 @@ object Epsilon1 {
 
   def rand(): Int = epsilon((x: Int) => true)
   def rand2(x: Int): Int = epsilon((y: Int) => true)
-  def rand3(x: Int): Int = epsilon((y: Int) => x == x)
 
   //this should hold, that is the expected semantic of our epsilon
   def property1(): Boolean = {
@@ -16,8 +15,4 @@ object Epsilon1 {
     rand2(x) == rand2(x+1) 
   } holds
 
-  //this should NOT hold
-  def property3(x: Int): Boolean = {
-    rand3(x) == rand3(x+1)
-  } holds
 }
diff --git a/testcases/regression/valid/Epsilon3.scala b/testcases/regression/valid/Epsilon3.scala
new file mode 100644
index 000000000..f652016d2
--- /dev/null
+++ b/testcases/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/testcases/regression/valid/Epsilon4.scala b/testcases/regression/valid/Epsilon4.scala
new file mode 100644
index 000000000..174042863
--- /dev/null
+++ b/testcases/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/testcases/regression/valid/Epsilon5.scala b/testcases/regression/valid/Epsilon5.scala
new file mode 100644
index 000000000..0427cf086
--- /dev/null
+++ b/testcases/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/testcases/regression/MyTuple3.scala b/testcases/regression/valid/MyTuple1.scala
similarity index 100%
rename from testcases/regression/MyTuple3.scala
rename to testcases/regression/valid/MyTuple1.scala
diff --git a/testcases/regression/MyTuple4.scala b/testcases/regression/valid/MyTuple2.scala
similarity index 82%
rename from testcases/regression/MyTuple4.scala
rename to testcases/regression/valid/MyTuple2.scala
index e928b2a9a..9fd21eb20 100644
--- a/testcases/regression/MyTuple4.scala
+++ b/testcases/regression/valid/MyTuple2.scala
@@ -1,4 +1,4 @@
-object MyTuple4 {
+object MyTuple2 {
 
   abstract class A
   case class B(i: Int) extends A
@@ -9,6 +9,6 @@ object MyTuple4 {
     t match {
       case (B(x), C(y)) => x
     }
-  } ensuring( _ > 0)
+  } ensuring(_ == 2)
 
 }
-- 
GitLab