stainless
stainless copied to clipboard
Aliasing information incorrectly tracked when conditions are modified
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
.