stainless icon indicating copy to clipboard operation
stainless copied to clipboard

Aliasing information incorrectly tracked when conditions are modified

Open mario-bucev opened this issue 2 years ago • 0 comments

Consider the following snippet:

object TargetMutatedCondition {
  case class Box(var value: Int)

  def test: Unit = {
    val b1 = Box(123)
    val b2 = Box(456)

    val b3 = if (b1.value == 123) {
      b1.value = 42
      b2
    } else Box(1)

    // b3 aliases b2

    assert(b1.value == 42) // Ok
    assert(b3.value == 456) // Ok

    b2.value = 5
    assert(b3.value == 5) // Invalid, but should not
  }
}

Here, b3 aliases b2 provided that b1.value == 123. But if we change b1.value (whether within the if statement or afterward), b3 still remains an alias of b2.

mario-bucev avatar Jun 09 '22 08:06 mario-bucev