From e7a5c6a65776d2e07a0286c3a1b4a032c7fda49a Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 19 Jan 2016 16:43:32 +0100
Subject: [PATCH] testcase for absolute value of array elements by reference
---
.../xlang/valid/ArrayParamMutation9.scala | 22 +++++++++++++++++++
1 file changed, 22 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
new file mode 100644
index 000000000..f5046b6cf
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+
+object ArrayParamMutation9 {
+ def abs(a: Array[Int]) {
+ require(a.length > 0)
+ var i = 0;
+ (while (i < a.length) {
+ a(i) = if (a(i) < 0) -a(i) else a(i) // <-- this makes Leon crash
+ i = i + 1
+ }) invariant(i >= 0)
+ }
+
+
+ def main = {
+ val a = Array(0, -1, 2, -3)
+
+ abs(a)
+
+ a(0) + a(1) - 1 + a(2) - 2 + a(3) - 3 // == 0
+ }
+
+}
--
GitLab