diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala new file mode 100644 index 0000000000000000000000000000000000000000..fcdc822b1cb9786d715051e61d3cf4b4c1acbb35 --- /dev/null +++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams6.scala @@ -0,0 +1,31 @@ +object HigherOrderFunctionsMutableParams6 { + + abstract class List + case class Cons(head: BigInt, tail: List) extends List + case class Nil() extends List + + case class A(var x: BigInt) + + def map(ls: List, f: (BigInt, A) => BigInt, a: A): List = ls match { + case Cons(head, tail) => + Cons(f(head, a), map(tail, f, a)) + + case Nil() => Nil() + } + + def fImpl(el: BigInt, a: A): BigInt = { + val last = a.x + a.x = el + last + } + + def shift(ls: List): List = { + val a = A(0) + map(ls, fImpl, a) + } + + def test(): List = { + val l = Cons(2, Cons(4, Cons(6, Nil()))) + shift(l) + } ensuring(res => res == Cons(0, Cons(2, Cons(4, Nil())))) +}