The following snippet is marked as invalid even though it is not:
import stainless.lang._
import stainless.annotation._
object VarVarBinks {
sealed trait OptionMut[@mutable T] {
def isDefined: Boolean = this match {
case SomeMut(_) => true
case NoneMut() => false
}
def get: T = {
require(isDefined)
this match {
case SomeMut(v) => v
}
}
}
// Note: v is not a var!
case class SomeMut[@mutable T](v: T) extends OptionMut[T]
case class NoneMut[@mutable T]() extends OptionMut[T]
case class C1(var f2: OptionMut[C2])
case class C2(var f3: OptionMut[C3])
case class C3(var v: BigInt)
def test(x: BigInt): BigInt = {
val c1 = C1(NoneMut())
c1.f2 = SomeMut(C2(NoneMut()))
c1.f2.get.f3 = SomeMut(C3(x))
c1.f2.get.f3.get.v // precond to f3.get is invalid
}
}
This is due to the field of SomeMut (v) being a val (declaring it a var makes the last expression go through as expected).
It seems that AntiAliasing is not correctly handling the update for c1.f2.get.f3 due to v not being a var.
The following snippet is marked as invalid even though it is not:
This is due to the field of
SomeMut
(v
) being aval
(declaring it avar
makes the last expression go through as expected). It seems thatAntiAliasing
is not correctly handling the update forc1.f2.get.f3
due tov
not being avar
.