Capture of this.v is too restrictive when v is a field of a mutable class this #1706
Description
example:
import stainless.collection.List
import stainless.lang.StaticChecks.*
object InternalMutationEx02 {
case class A(val v: BigInt, var m: BigInt) {
def f(): BigInt => BigInt = x => v // stainless consider this.v to capture the mutable object this, even though v is immutable, because it is a field of a mutable object.
}
}this is currently rejected:
❯ stainless field_val_capture.scala
[ Info ] Finished compiling
[ Info ] Preprocessing finished
[ Info ] Running phase AntiAliasing
[ Fatal ] field_val_capture.scala:6:33: Illegal capturing of variables with mutable type: thiss
def f(): BigInt => BigInt = x => v // stainless consider this.v to capture the mutable object this, even though v is immutable, because it is a field of a mutable object.
^^^^^^
[ Error ] Stainless terminated with an error.
[ Error ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error ] You may use --debug=stack to have the stack trace displayed in the output.
However, it should not consider that it captures the mutable this when we only access an immutable field whose type is immutable.
Metadata
Metadata
Assignees
Labels
No labels