more aliasing restrictions

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 _ => ()
       }
     }

src/test/resources/regression/xlang/error/ObjectAliasing5.scala

+import leon.lang._
+
+object ObjectAliasing5 {
+
+  case class A(var x: Int)
+  case class B(a: A)
+
+  def f1(b: B): A = {
+    b.a
+  }
+
+}

src/test/resources/regression/xlang/error/ObjectAliasing6.scala

+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)
+
+}

src/test/resources/regression/xlang/error/ObjectAliasing7.scala

+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)
+
+}