From 5b2cf2cba19a3d321228887c525636cdccef8f0a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 12 Dec 2012 14:36:56 +0100
Subject: [PATCH] new regression tests on Tuple in purescala
---
.../purescala/invalid/MyTuple1.scala | 11 +++++++++++
.../purescala/invalid/MyTuple2.scala | 14 ++++++++++++++
.../purescala/invalid/MyTuple3.scala | 7 +++++++
.../verification/purescala/valid/MyTuple1.scala | 11 +++++++++++
.../verification/purescala/valid/MyTuple2.scala | 14 ++++++++++++++
.../verification/purescala/valid/MyTuple3.scala | 8 ++++++++
.../verification/purescala/valid/MyTuple4.scala | 14 ++++++++++++++
.../verification/purescala/valid/MyTuple5.scala | 16 ++++++++++++++++
.../verification/purescala/valid/MyTuple6.scala | 8 ++++++++
9 files changed, 103 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
new file mode 100644
index 000000000..f2b06b5b2
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
new file mode 100644
index 000000000..22b62dc75
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
new file mode 100644
index 000000000..da9f85b16
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
new file mode 100644
index 000000000..48383898e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
new file mode 100644
index 000000000..9fd21eb20
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
new file mode 100644
index 000000000..2e14c067b
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
new file mode 100644
index 000000000..6fcfed661
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
new file mode 100644
index 000000000..6a55bc8c9
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
new file mode 100644
index 000000000..a54710fbb
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/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)
+
+}
--
GitLab