From 4b5362ddd20ede386d5be877176f0409af2d0ba3 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 13 Jan 2016 17:25:39 +0100
Subject: [PATCH] first batch of tests for array mutation
---
build.sbt | 4 ++--
.../scala/leon/xlang/AntiAliasingPhase.scala | 2 --
.../xlang/valid/ArrayParamMutation1.scala | 16 +++++++++++++
.../xlang/valid/ArrayParamMutation2.scala | 16 +++++++++++++
.../xlang/valid/ArrayParamMutation3.scala | 23 +++++++++++++++++++
.../xlang/valid/ArrayParamMutation4.scala | 23 +++++++++++++++++++
.../xlang/valid/ArrayParamMutation5.scala | 21 +++++++++++++++++
.../xlang/valid/ArrayParamMutation6.scala | 16 +++++++++++++
8 files changed, 117 insertions(+), 4 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
diff --git a/build.sbt b/build.sbt
index 0e3e147a1..4ecb2f93a 100644
--- a/build.sbt
+++ b/build.sbt
@@ -109,8 +109,8 @@ Keys.fork in run := true
lazy val testSettings = Seq(
//Keys.fork := true,
- logBuffered := true,
- parallelExecution := true
+ logBuffered := false,
+ parallelExecution := false
//testForkedParallel := true,
//javaOptions ++= Seq("-Xss64M", "-Xmx4G")
)
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index a7adbfbaa..f9610904c 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -262,7 +262,6 @@ object AntiAliasingPhase extends TransformationPhase {
}
}
-
def invocEffects(fi: FunctionInvocation): Set[Identifier] = {
if(!effects.isDefinedAt(fi.tfd.fd)) {
println("fi not defined: " + fi)
@@ -276,7 +275,6 @@ object AntiAliasingPhase extends TransformationPhase {
}.toSet
}
-
rec()
effects
}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
new file mode 100644
index 000000000..f0e622c66
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation1 {
+
+ def update(a: Array[BigInt]): Unit = {
+ require(a.length > 0)
+ a(0) = 10
+ }
+
+ def f(): BigInt = {
+ val a = Array.fill(10)(BigInt(0))
+ update(a)
+ a(0)
+ } ensuring(res => res == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
new file mode 100644
index 000000000..801b35e0c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation2 {
+
+ def rec(a: Array[BigInt]): BigInt = {
+ require(a.length > 1 && a(0) >= 0)
+ if(a(0) == 0)
+ a(1)
+ else {
+ a(0) = a(0) - 1
+ a(1) = a(1) + a(0)
+ rec(a)
+ }
+ } ensuring(res => a(0) == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
new file mode 100644
index 000000000..f57516744
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object ArrayParamMutation3 {
+
+ def odd(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) false
+ else {
+ a(0) = a(0) - 1
+ even(a)
+ }
+ } ensuring(res => a(0) == 0)
+
+ def even(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) true
+ else {
+ a(0) = a(0) - 1
+ odd(a)
+ }
+ } ensuring(res => a(0) == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
new file mode 100644
index 000000000..31af4cd58
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object ArrayParamMutation4 {
+
+ def multipleArgs(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ if(a1(0) == 10)
+ a2(0) = 13
+ else
+ a2(0) = a1(0) + 1
+ }
+
+ def transitiveEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ multipleArgs(a1, a2)
+ } ensuring(_ => a2(0) >= a1(0))
+
+ def transitiveReverseEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ multipleArgs(a2, a1)
+ } ensuring(_ => a1(0) >= a2(0))
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
new file mode 100644
index 000000000..249a79d1f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
@@ -0,0 +1,21 @@
+
+import leon.lang._
+
+object ArrayParamMutation5 {
+
+ def mutuallyRec1(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a1(0) > 0 && a2.length > 0)
+ if(a1(0) == 10) {
+ ()
+ } else {
+ mutuallyRec2(a1, a2)
+ }
+ } ensuring(res => a1(0) == 10)
+
+ def mutuallyRec2(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0 && a1(0) > 0)
+ a1(0) = 10
+ mutuallyRec1(a1, a2)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
new file mode 100644
index 000000000..29ded427f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation6 {
+
+ def multipleEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ a1(0) = 11
+ a2(0) = 12
+ } ensuring(_ => a1(0) != a2(0))
+
+ def f(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+ require(a1.length > 0 && a2.length > 0)
+ multipleEffects(a1, a2)
+ } ensuring(_ => a1(0) == 11 && a2(0) == 12)
+
+}
--
GitLab