From 84cba1ccd83254165eccd0c98d79961d0d3b83a1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 25 Sep 2015 18:11:28 +0200
Subject: [PATCH] Move non-XLang tests to purescala
---
.../invalid/Array5.scala} | 2 +-
.../invalid/Array6.scala} | 2 +-
.../invalid/Array7.scala} | 2 +-
.../{xlang => purescala}/invalid/Mean.scala | 0
.../valid => purescala/invalid}/Nested15.scala | 5 ++---
.../valid/Array1.scala} | 2 +-
.../valid/Array2.scala} | 2 +-
.../valid/Array3.scala} | 2 +-
.../valid/Choose2.scala} | 2 +-
.../{xlang => purescala}/valid/Mean.scala | 0
.../{xlang => purescala}/valid/Nested1.scala | 0
.../{xlang => purescala}/valid/Nested10.scala | 0
.../{xlang => purescala}/valid/Nested11.scala | 0
.../{xlang => purescala}/valid/Nested12.scala | 0
.../{xlang => purescala}/valid/Nested13.scala | 0
.../{xlang => purescala}/valid/Nested14.scala | 0
.../verification/purescala/valid/Nested15.scala | 17 +++++++++++++++++
.../{xlang => purescala}/valid/Nested2.scala | 0
.../{xlang => purescala}/valid/Nested3.scala | 0
.../{xlang => purescala}/valid/Nested4.scala | 0
.../{xlang => purescala}/valid/Nested5.scala | 0
.../{xlang => purescala}/valid/Nested6.scala | 0
.../{xlang => purescala}/valid/Nested7.scala | 0
.../{xlang => purescala}/valid/Nested8.scala | 0
.../{xlang => purescala}/valid/Nested9.scala | 0
.../invalid/{Asserts.scala => Asserts2.scala} | 2 +-
26 files changed, 27 insertions(+), 11 deletions(-)
rename src/test/resources/regression/verification/{xlang/invalid/Array4.scala => purescala/invalid/Array5.scala} (87%)
rename src/test/resources/regression/verification/{xlang/invalid/Array5.scala => purescala/invalid/Array6.scala} (90%)
rename src/test/resources/regression/verification/{xlang/invalid/Array6.scala => purescala/invalid/Array7.scala} (91%)
rename src/test/resources/regression/verification/{xlang => purescala}/invalid/Mean.scala (100%)
rename src/test/resources/regression/verification/{xlang/valid => purescala/invalid}/Nested15.scala (82%)
rename src/test/resources/regression/verification/{xlang/valid/Array6.scala => purescala/valid/Array1.scala} (93%)
rename src/test/resources/regression/verification/{xlang/valid/Array8.scala => purescala/valid/Array2.scala} (92%)
rename src/test/resources/regression/verification/{xlang/valid/Array9.scala => purescala/valid/Array3.scala} (93%)
rename src/test/resources/regression/verification/{xlang/valid/Choose1.scala => purescala/valid/Choose2.scala} (92%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Mean.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested1.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested10.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested11.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested12.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested13.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested14.scala (100%)
create mode 100644 src/test/resources/regression/verification/purescala/valid/Nested15.scala
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested2.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested3.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested4.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested5.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested6.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested7.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested8.scala (100%)
rename src/test/resources/regression/verification/{xlang => purescala}/valid/Nested9.scala (100%)
rename src/test/resources/regression/verification/xlang/invalid/{Asserts.scala => Asserts2.scala} (93%)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array4.scala b/src/test/resources/regression/verification/purescala/invalid/Array5.scala
similarity index 87%
rename from src/test/resources/regression/verification/xlang/invalid/Array4.scala
rename to src/test/resources/regression/verification/purescala/invalid/Array5.scala
index 111d4e3a4..2adb7e5c5 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array4.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array5.scala
@@ -2,7 +2,7 @@
import leon.lang._
-object Array4 {
+object Array5 {
def foo(a: Array[Int]): Int = {
a(2)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/purescala/invalid/Array6.scala
similarity index 90%
rename from src/test/resources/regression/verification/xlang/invalid/Array5.scala
rename to src/test/resources/regression/verification/purescala/invalid/Array6.scala
index 32a12648f..18a1e7ab0 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array5.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array6.scala
@@ -2,7 +2,7 @@
import leon.lang._
-object Array5 {
+object Array6 {
def foo(a: Array[Int]): Int = {
require(a.length > 2)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array6.scala b/src/test/resources/regression/verification/purescala/invalid/Array7.scala
similarity index 91%
rename from src/test/resources/regression/verification/xlang/invalid/Array6.scala
rename to src/test/resources/regression/verification/purescala/invalid/Array7.scala
index 5e0aded33..dcf7059f8 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array6.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array7.scala
@@ -2,7 +2,7 @@
import leon.lang._
-object Array6 {
+object Array7 {
def foo(a: Array[Int]): Int = {
require(a.length > 0)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Mean.scala b/src/test/resources/regression/verification/purescala/invalid/Mean.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/invalid/Mean.scala
rename to src/test/resources/regression/verification/purescala/invalid/Mean.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested15.scala b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
similarity index 82%
rename from src/test/resources/regression/verification/xlang/valid/Nested15.scala
rename to src/test/resources/regression/verification/purescala/invalid/Nested15.scala
index 490404f86..228afa9fa 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested15.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.collection._
-object Nested1 {
+object Nested15 {
def foo[A](i: List[A]): BigInt = {
val n = i
@@ -11,8 +11,7 @@ object Nested1 {
rec3(l.head).size + j + n.size + i.size
}
rec2(List(true, true, false), 2)
- } ensuring(i.size + 7 == _)
+ } ensuring(_ == i.size + 9) // Should be 2* size
}
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/purescala/valid/Array1.scala
similarity index 93%
rename from src/test/resources/regression/verification/xlang/valid/Array6.scala
rename to src/test/resources/regression/verification/purescala/valid/Array1.scala
index ec477eb30..4dbec292c 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array6.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Array1.scala
@@ -2,7 +2,7 @@
import leon.lang._
-object Array6 {
+object Array1 {
def foo(a: Array[Int]): Int = {
require(a.length > 2 && a(2) == 5)
diff --git a/src/test/resources/regression/verification/xlang/valid/Array8.scala b/src/test/resources/regression/verification/purescala/valid/Array2.scala
similarity index 92%
rename from src/test/resources/regression/verification/xlang/valid/Array8.scala
rename to src/test/resources/regression/verification/purescala/valid/Array2.scala
index 29c1b686c..53d30e9af 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array8.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Array2.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-object Array8 {
+object Array2 {
def foo(a: Array[Int]): Array[Int] = {
require(a.length >= 2)
diff --git a/src/test/resources/regression/verification/xlang/valid/Array9.scala b/src/test/resources/regression/verification/purescala/valid/Array3.scala
similarity index 93%
rename from src/test/resources/regression/verification/xlang/valid/Array9.scala
rename to src/test/resources/regression/verification/purescala/valid/Array3.scala
index 10140b9c1..b7ea754b4 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array9.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Array3.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-object Array9 {
+object Array3 {
def foo(i: Int): Array[Int] = {
require(i > 0)
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose2.scala
similarity index 92%
rename from src/test/resources/regression/verification/xlang/valid/Choose1.scala
rename to src/test/resources/regression/verification/purescala/valid/Choose2.scala
index 380be2148..ad05bda10 100644
--- a/src/test/resources/regression/verification/xlang/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Choose2.scala
@@ -3,7 +3,7 @@
import leon.lang._
import leon.lang.synthesis._
-object Choose1 {
+object Choose2 {
def test(x: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Mean.scala b/src/test/resources/regression/verification/purescala/valid/Mean.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Mean.scala
rename to src/test/resources/regression/verification/purescala/valid/Mean.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested1.scala b/src/test/resources/regression/verification/purescala/valid/Nested1.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested1.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested1.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested10.scala b/src/test/resources/regression/verification/purescala/valid/Nested10.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested10.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested10.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested11.scala b/src/test/resources/regression/verification/purescala/valid/Nested11.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested11.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested11.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested12.scala b/src/test/resources/regression/verification/purescala/valid/Nested12.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested12.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested12.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested13.scala b/src/test/resources/regression/verification/purescala/valid/Nested13.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested13.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested13.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested14.scala b/src/test/resources/regression/verification/purescala/valid/Nested14.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested14.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested14.scala
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested15.scala b/src/test/resources/regression/verification/purescala/valid/Nested15.scala
new file mode 100644
index 000000000..a81c77e67
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nested15.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.collection._
+object Nested15 {
+
+ def foo[A](i: List[A]): BigInt = {
+ val n = i
+ def rec1[B](j: List[B]) = j ++ j
+ def rec2[C](l: List[C], j: BigInt) = {
+ require(l.nonEmpty)
+ def rec3(k: C) = k :: rec1[C](l)
+ rec3(l.head).size + j + n.size + i.size
+ }
+ rec2(List(true, true, false), 2)
+ } ensuring(_ == 2 * i.size + 9)
+
+}
+
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested2.scala b/src/test/resources/regression/verification/purescala/valid/Nested2.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested2.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested2.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested3.scala b/src/test/resources/regression/verification/purescala/valid/Nested3.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested3.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested3.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested4.scala b/src/test/resources/regression/verification/purescala/valid/Nested4.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested4.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested4.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested5.scala b/src/test/resources/regression/verification/purescala/valid/Nested5.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested5.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested5.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/purescala/valid/Nested6.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested6.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested6.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/purescala/valid/Nested7.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested7.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested7.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/purescala/valid/Nested8.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested8.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested8.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/purescala/valid/Nested9.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested9.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested9.scala
diff --git a/src/test/resources/regression/verification/xlang/invalid/Asserts.scala b/src/test/resources/regression/verification/xlang/invalid/Asserts2.scala
similarity index 93%
rename from src/test/resources/regression/verification/xlang/invalid/Asserts.scala
rename to src/test/resources/regression/verification/xlang/invalid/Asserts2.scala
index 3540c98dd..bfda82471 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Asserts.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Asserts2.scala
@@ -4,7 +4,7 @@ import leon.annotation._
import leon.lang._
import leon.lang._
-object Asserts {
+object Asserts2 {
def assert1(i: BigInt): BigInt = { // we might define assert like so
require(i >= 0)
--
GitLab