Wrong imperative translation when mutable object returned (AntiAliasing, effects)

[vkuncak]

This verifies on master as of today:

object Test {
  case class IntRef(var x:Int)
  def f = IntRef(42)

  def g(d1: IntRef, d2: IntRef) = {
    val x1 = d1.x
    d2.x = 33
    assert(d1.x==x1)
  }
  
  def mytest:Unit = {
    val c1 = f
    val c2 = c1
    g(c1, c2)
  }
}

Running Test.mytest in scala REPL crashes in assertion, as I would expect.

[vkuncak]

"The aliasing check in function invocation arguments is pretty useless...

stainless/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

Line 437 in 43aa5c7

args.find { case v: Variable => vis.contains(v) case _ => false }

aliasing can occur with fields, e.g. a.b and a.b are aliased which won't be caught by the check
We can probably do something like finding conservative targets using Try(getTargets(e)).toOption.getOrElse(variablesOf(e))
"

[jad-hamza]

Fixed by PR #965