Swap operation on references #1356
Description
This code is unfortunately not accepted by alias analysis.
import stainless.lang.*
object Tree {
sealed abstract class Tree
case class Node(var left: Tree, var x: Int, var right: Tree) extends Tree
case class Leaf() extends Tree
def flip(t: Tree): Unit = {
t match
case Leaf() => ()
case _ =>
val n: Node = t.asInstanceOf[Node]
val tmp = n.right
n.right = n.left
n.left = tmp
}
}If this is inherent to how we track aliases, maybe we can come up with a primitive to do a swap, like the one we have with the arrays. One question is how to refer to a pair of an object and a field.