testing higher order function with mutable parameters

src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams1.scala

+object HigherOrderFunctionsMutableParams1 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => Unit, a: A): Unit = {
+    f(a)
+  }
+
+  def fImpl(a: A): Unit = {
+    a.x += 1
+  }
+
+
+  def test(): BigInt = {
+    val a = A(0)
+    app(fImpl, a)
+    assert(a.x == 1)
+    app(fImpl, a)
+    assert(a.x == 2)
+    app(fImpl, a)
+    a.x
+  } ensuring(_ == 3)
+
+}

src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams2.scala

+object HigherOrderFunctionsMutableParams2 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => BigInt, a: A): BigInt = {
+    f(a)
+  }
+
+  def fImpl(a: A): BigInt = {
+    a.x += 1
+    a.x
+  }
+
+
+  def test(): BigInt = {
+    val a = A(0)
+    app(fImpl, a)
+    app(fImpl, a)
+    app(fImpl, a)
+  } ensuring(_ == 3)
+
+}

src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams3.scala

+object HigherOrderFunctionsMutableParams3 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => BigInt, a: A): BigInt = {
+    f(a)
+  }
+
+  def fImpl1(a: A): BigInt = {
+    a.x += 1
+    a.x
+  }
+  def fImpl2(a: A): BigInt = {
+    a.x += 10
+    a.x
+  }
+
+
+  def test(): BigInt = {
+    val a = A(0)
+    app(fImpl1, a)
+    app(fImpl2, a)
+    app(fImpl1, a)
+  } ensuring(_ == 12)
+
+}

src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams4.scala

+object HigherOrderFunctionsMutableParams4 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => BigInt, a: A): BigInt = {
+    f(a)
+  }
+
+  def test(): BigInt = {
+    val a = A(0)
+    app((a2: A) => {
+      a2.x += 1
+      a2.x
+    }, a)
+    app((a2: A) => {
+      a2.x += 10
+      a2.x
+    }, a)
+    app((a2: A) => {
+      a2.x += 1
+      a2.x
+    }, a)
+  } ensuring(_ == 12)
+
+}