array copy testcase to prove

src/main/scala/leon/xlang/AntiAliasingPhase.scala

@@ -252,7 +252,8 @@ object AntiAliasingPhase extends TransformationPhase {
         val duplicatedParams = allParams.diff(allParams.distinct).distinct
         if(duplicatedParams.nonEmpty) 
           ctx.reporter.fatalError(nfi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head)
-        //TODO: we are probably missing a case with multiple same variable within one same argument (f(A(x1,x1,x1)))
+        //TODO: The case f(A(x1,x1,x1)) could probably be handled by forbidding creation at any program point of
+        //      case class with multiple refs as it is probably not useful
 
         val freshRes = FreshIdentifier("res", nfiType)
 

testcases/verification/xlang/arrays/ArrayCopy.scala

@@ -0,0 +1,36 @@
+import leon.lang._
+
+object ArrayCopy {
+
+  def copy(source: Array[Int], dest: Array[Int]): Unit = {
+    require(source.length > 0 && source.length <= dest.length)
+    val sourceLength = source.length
+
+    var i = 0
+    (while (i < source.length) {
+      dest(i) = source(i)
+      i = i + 1
+    }) invariant {
+      i >= 0 && i <= source.length &&
+      (i == 0 || same(source, dest, 0, i)) &&
+      source.length <= dest.length &&
+      source.length == sourceLength 
+    }
+
+  } ensuring { _ => {
+    source.length == old(source).length &&
+    same(source, old(source), 0, source.length) && 
+    source.length <= dest.length &&
+    same(source, dest, 0, source.length)
+  }}
+
+  def same(a1: Array[Int], a2: Array[Int], from: Int, to: Int): Boolean = {
+    require(from >= 0 && from <= a1.length && from <= a2.length && 
+            to >= from && to <= a1.length && to <= a2.length)
+
+    if(from == to || from == to) true
+    else a1(from) == a2(from) && same(a1, a2, from+1, to)
+  }
+
+
+}