Closed yannbolliger closed 3 years ago
val s = var0
works for this one, but I don't know if that's good enough for your use case?
Take-away from the discussion with @jad-hamza:
snapshot
. It tells Stainless that we operate on a new copy/version of the ADT that no one else has access to. This is the same as the idea of the @owned
flag, @romac suggested.@pure
because they only operate on the new copy of the params.@var
.
Stainless doesn't distinguish between owned objects and referenced/shared/borrowed objects, because on the JVM every object is a reference. Therefore,
AntiAliasing
in Stainless hinders the Rust frontend to pass such code:Which corresponds to the following in Scala (and is transformed to it by the Rust frontend's extraction). Internally, the
mut s: S
is translated to aLetVar
at the beginning of the function:But this is not allowed in Stainless, because Stainless can't see that the parameter
var0
is consumed/owned and can be modified at will. Neither does it see thatvar0
is not used after theLetVar
assignment. Finally, Stainless fails withIllegal Aliasing: var0
.