From 20ae5a95330674322fc7304c4ab0f5d9987f2ca5 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 26 Oct 2015 12:51:57 +0100
Subject: [PATCH] basic support in nested functions for arrays
---
.../frontends/scalac/CodeExtraction.scala | 8 ++++----
.../xlang/valid/ArrayNested1.scala | 19 +++++++++++++++++++
.../xlang/valid/ArrayNested2.scala | 19 +++++++++++++++++++
3 files changed, 42 insertions(+), 4 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index a232b93da..24ecca501 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1200,11 +1200,11 @@ trait CodeExtraction extends ASTExtractors {
}
getOwner(lhsRec) match {
- case Some(Some(fd)) if fd != currentFunDef =>
- outOfSubsetError(tr, "cannot update an array that is not defined locally")
+ // case Some(Some(fd)) if fd != currentFunDef =>
+ // outOfSubsetError(tr, "cannot update an array that is not defined locally")
- case Some(None) =>
- outOfSubsetError(tr, "cannot update an array that is not defined locally")
+ // case Some(None) =>
+ // outOfSubsetError(tr, "cannot update an array that is not defined locally")
case Some(_) =>
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala
new file mode 100644
index 000000000..196a6442b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ArrayNested1 {
+
+ def test(): Int = {
+
+ var a = Array(1, 2, 0)
+
+ def nested(): Unit = {
+ require(a.length == 3)
+ a = a.updated(1, 5)
+ }
+
+ nested()
+ a(1)
+
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
new file mode 100644
index 000000000..fb1a778b8
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ArrayNested2 {
+
+ def test(): Int = {
+
+ var a = Array(1, 2, 0)
+
+ def nested(): Unit = {
+ require(a.length == 3)
+ a(2) = 5
+ }
+
+ nested()
+ a(2)
+
+ } ensuring(_ == 5)
+
+}
--
GitLab