From d12b44a6fdc141b6cfe6c37b594377fb36bd32dd Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 17 Mar 2016 13:13:05 +0100
Subject: [PATCH] more aliasing restrictions
---
.../scala/leon/xlang/AntiAliasingPhase.scala | 7 ++++--
.../xlang/error/ObjectAliasing5.scala | 12 ++++++++++
.../xlang/error/ObjectAliasing6.scala | 14 ++++++++++++
.../xlang/error/ObjectAliasing7.scala | 22 +++++++++++++++++++
4 files changed, 53 insertions(+), 2 deletions(-)
create mode 100644 src/test/resources/regression/xlang/error/ObjectAliasing5.scala
create mode 100644 src/test/resources/regression/xlang/error/ObjectAliasing6.scala
create mode 100644 src/test/resources/regression/xlang/error/ObjectAliasing7.scala
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 70163481f..9eaf5eb33 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -332,8 +332,11 @@ object AntiAliasingPhase extends TransformationPhase {
def checkAliasing(fd: FunDef)(ctx: LeonContext): Unit = {
def checkReturnValue(body: Expr, bindings: Set[Identifier]): Unit = {
getReturnedExpr(body).foreach{
- case IsTyped(v@Variable(id), tpe) if isMutableType(tpe) && bindings.contains(id) =>
- ctx.reporter.fatalError(v.getPos, "Cannot return a shared reference to a mutable object: " + v)
+ case expr if isMutableType(expr.getType) =>
+ findReceiverId(expr).foreach(id =>
+ if(bindings.contains(id))
+ ctx.reporter.fatalError(expr.getPos, "Cannot return a shared reference to a mutable object: " + expr)
+ )
case _ => ()
}
}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing5.scala b/src/test/resources/regression/xlang/error/ObjectAliasing5.scala
new file mode 100644
index 000000000..c94656fdb
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing5.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+
+object ObjectAliasing5 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(b: B): A = {
+ b.a
+ }
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing6.scala b/src/test/resources/regression/xlang/error/ObjectAliasing6.scala
new file mode 100644
index 000000000..793b9815d
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing6.scala
@@ -0,0 +1,14 @@
+import leon.lang._
+
+object ObjectAliasing6 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(b: B): Int = {
+ val a = b.a
+ a.x = 12
+ b.a.x
+ } ensuring(_ == 12)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ObjectAliasing7.scala b/src/test/resources/regression/xlang/error/ObjectAliasing7.scala
new file mode 100644
index 000000000..ea28fa5bb
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ObjectAliasing7.scala
@@ -0,0 +1,22 @@
+package test.resources.regression.xlang.error
+
+import leon.lang._
+
+object ObjectAliasing7 {
+
+ case class A(var x: Int)
+ case class B(a: A)
+
+ def f1(a1: A, a2: A): Int = {
+ val tmp = a1.x
+ a2.x = a1.x
+ a1.x = tmp
+ a1.x + a2.x
+ }
+
+ def f(): Int = {
+ val b = B(A(10))
+ f1(b.a, b.a)
+ } ensuring(_ == 20)
+
+}
--
GitLab