From 88981f3260158f484d190098be0eb3538c2c01b6 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 3 Feb 2016 19:51:17 +0100
Subject: [PATCH] more testing
---
.../valid/NestedFunParamsMutation1.scala | 16 ++++++++++++++
.../valid/NestedFunParamsMutation2.scala | 21 +++++++++++++++++++
.../xlang/error/ArrayAliasing10.scala | 19 +++++++++++++++++
3 files changed, 56 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
create mode 100644 src/test/resources/regression/xlang/error/ArrayAliasing10.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
new file mode 100644
index 000000000..a7250a7bc
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object NestedFunParamsMutation1 {
+
+ def f(): Int = {
+ def g(a: Array[Int]): Unit = {
+ require(a.length > 0)
+ a(0) = 10
+ }
+
+ val a = Array(1,2,3,4)
+ g(a)
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
new file mode 100644
index 000000000..799a87c6e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+
+object NestedFunParamsMutation2 {
+
+ def f(): Int = {
+ def g(a: Array[Int]): Unit = {
+ require(a.length > 0)
+ a(0) = 10
+ }
+
+ def h(a: Array[Int]): Unit = {
+ require(a.length > 0)
+ g(a)
+ }
+
+ val a = Array(1,2,3,4)
+ h(a)
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing10.scala b/src/test/resources/regression/xlang/error/ArrayAliasing10.scala
new file mode 100644
index 000000000..05737b03d
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing10.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object ArrayAliasing10 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+
+ def rec(): Array[Int] = {
+
+ def nestedRec(): Array[Int] = {
+ a
+ }
+ nestedRec()
+ }
+ val b = rec()
+ b(0)
+ }
+
+}
--
GitLab