From e5dd347bf40e2f72912bcab68d1e96b185bbb08f Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 9 Feb 2016 15:30:10 +0100
Subject: [PATCH] testing aliasing to captured variables
---
.../xlang/error/NestedFunctionAliasing1.scala | 17 +++++++++++++++++
.../xlang/error/NestedFunctionAliasing2.scala | 17 +++++++++++++++++
2 files changed, 34 insertions(+)
create mode 100644 src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
create mode 100644 src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
diff --git a/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala b/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
new file mode 100644
index 000000000..12feace54
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object NestedFunctinAliasing1 {
+
+ def f(): Int = {
+ val a = Array(1,2,3,4)
+
+ def g(b: Array[Int]): Unit = {
+ require(b.length > 0 && a.length > 0)
+ b(0) = 10
+ a(0) = 17
+ } ensuring(_ => b(0) == 10)
+
+ g(a)
+ a(0)
+ } ensuring(_ == 10)
+}
diff --git a/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala b/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
new file mode 100644
index 000000000..81a9b82b3
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object NestedFunctinAliasing1 {
+
+ def f(a: Array(1,2,3,4)): Int = {
+
+ def g(b: Array[Int]): Unit = {
+ require(b.length > 0 && a.length > 0)
+ b(0) = 10
+ a(0) = 17
+ } ensuring(_ => b(0) == 10)
+
+ g(a)
+ a(0)
+ } ensuring(_ == 10)
+
+}
--
GitLab