From 63f108bb99bc9fb0298579ab3ab254b4e84d4024 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 14 Jan 2016 16:43:43 +0100
Subject: [PATCH] new limitation check for aliasing

---
 .../scala/leon/xlang/AntiAliasingPhase.scala  | 19 +++++++++++++++++++
 .../xlang/error/ArrayAliasing4.scala          | 11 +++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 src/test/resources/regression/xlang/error/ArrayAliasing4.scala

diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index f9610904c..066319377 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -60,6 +60,12 @@ object AntiAliasingPhase extends TransformationPhase {
       case _ => None
     }.map(_.id)
 
+    fd.body.foreach(body => getReturnedExpr(body).foreach{
+      case v@Variable(id) if aliasedParams.contains(id) =>
+        ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object")
+      case _ => ()
+    })
+
     val newReturnType: TypeTree = if(aliasedParams.isEmpty) fd.returnType else {
       tupleTypeWrap(fd.returnType +: aliasedParams.map(_.getType))
     }
@@ -280,4 +286,17 @@ object AntiAliasingPhase extends TransformationPhase {
   }
 
 
+  /*
+   * A bit hacky, but not sure of the best way to do something like that
+   * currently.
+   */
+  private def getReturnedExpr(expr: Expr): Seq[Expr] = expr match {
+    case Let(_, _, rest) => getReturnedExpr(rest)
+    case LetVar(_, _, rest) => getReturnedExpr(rest)
+    case Block(_, rest) => getReturnedExpr(rest)
+    case IfExpr(_, thenn, elze) => getReturnedExpr(thenn) ++ getReturnedExpr(elze)
+    case MatchExpr(_, cses) => cses.flatMap{ cse => getReturnedExpr(cse.rhs) }
+    case e => Seq(expr)
+  }
+
 }
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing4.scala b/src/test/resources/regression/xlang/error/ArrayAliasing4.scala
new file mode 100644
index 000000000..2632782c3
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing4.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing4 {
+
+  def f1(a: Array[BigInt]): Array[BigInt] = {
+    require(a.length > 0)
+    a(0) = 10
+    a
+  } ensuring(res => res(0) == 10)
+
+}
-- 
GitLab