relaxing the fix

epfl-lara · Feb 14, 2017 · 96bae6a · 96bae6a
1 parent 5cbde5e
commit 96bae6a
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/src/main/scala/leon/xlang/EffectsChecking.scala b/src/main/scala/leon/xlang/EffectsChecking.scala
@@ -106,7 +106,7 @@ object EffectsChecking extends UnitPhase[Program] {
       getReturnedExpr(body).foreach{
         case expr if effects.isMutableType(expr.getType) => 
           findReferencedIds(expr).foreach(id =>
-            if(bindings.contains(id))
+            if(effects.isMutableType(id.getType) && 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/passing/ReturnNoAliasing1.scala b/src/test/resources/regression/xlang/passing/ReturnNoAliasing1.scala
@@ -0,0 +1,9 @@
+import leon.lang._
+
+object ReturnNoAliasing1 {
+
+  case class A(var x: Int)
+
+  def f(y: Int): A = A(y)
+
+}