From 49c6e436d8b583174a0de17e96a826d81c9ae6c2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 19 Jan 2016 16:00:40 +0100
Subject: [PATCH] test world passing implicitly
---
.../xlang/valid/ArrayParamMutation7.scala | 29 +++++++++++++++++++
1 file changed, 29 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
new file mode 100644
index 000000000..53d67729f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+
+object ArrayParamMutation7 {
+
+ def f(i: BigInt)(implicit world: Array[BigInt]): BigInt = {
+ require(world.length == 3)
+
+ world(1) += 1 //global counter of f
+
+ val res = i*i
+ world(0) = res
+ res
+ }
+
+ def mainProgram(): Unit = {
+
+ implicit val world: Array[BigInt] = Array(0,0,0)
+
+ f(1)
+ assert(world(0) == 1)
+ f(2)
+ assert(world(0) == 4)
+ f(4)
+ assert(world(0) == 16)
+
+ assert(world(1) == 3)
+ }
+
+}
--
GitLab