From 520b16bb42ddc3c02e664fe0bbde8cc177eddcba Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 18 Jan 2016 15:07:06 +0100
Subject: [PATCH] detect multiple passing same argument
---
.../scala/leon/xlang/AntiAliasingPhase.scala | 5 ++++-
.../xlang/error/ArrayAliasing5.scala | 18 ++++++++++++++++++
2 files changed, 22 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/xlang/error/ArrayAliasing5.scala
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 066319377..8a5f627a7 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -1,5 +1,4 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-
package leon.xlang
import leon.TransformationPhase
@@ -177,6 +176,10 @@ object AntiAliasingPhase extends TransformationPhase {
args.zipWithIndex.filter{ case (arg, i) => fiEffects.contains(i) }
.map(_._1.asInstanceOf[Variable])
+ val duplicatedParams = modifiedArgs.diff(modifiedArgs.distinct).distinct
+ if(duplicatedParams.nonEmpty)
+ ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head)
+
val freshRes = FreshIdentifier("res", nfd.returnType)
val extractResults = Block(
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing5.scala b/src/test/resources/regression/xlang/error/ArrayAliasing5.scala
new file mode 100644
index 000000000..b9363d1ab
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing5.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object ArrayAliasing5 {
+
+
+ def f1(a: Array[BigInt], b: Array[BigInt]): Unit = {
+ require(a.length > 0 && b.length > 0)
+ a(0) = 10
+ b(0) = 20
+ } ensuring(_ => a(0) == 10 && b(0) == 20)
+
+
+ def callWithAliases(): Unit = {
+ val a = Array[BigInt](0,0,0,0)
+ f1(a, a)
+ }
+
+}
--
GitLab