implement missing ArrayUpdated in codegen

src/main/scala/leon/codegen/CodeGeneration.scala

@@ -346,6 +346,30 @@ trait CodeGeneration {
           case _ => AALOAD
         })
 
+      case au @ ArrayUpdated(a, i, v) =>
+        mkExpr(a, ch)
+        ch << DUP
+        ch << ARRAYLENGTH
+        val storeInstr = a.getType match {
+          case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
+          case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
+          case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
+          case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
+        } 
+        //srcArrary and targetArray is on the stack
+        ch << DUP_X1 //insert targetArray under srcArray
+        ch << Ldc(0) << SWAP //srcArray, 0, targetArray
+        ch << DUP << ARRAYLENGTH //targetArray, length on stack
+        ch << Ldc(0) << SWAP //final arguments: src, 0, target, 0, length
+        ch << InvokeStatic("java/lang/System", "arraycopy", "(Ljava/lang/Object;ILjava/lang/Object;II)V")
+
+        //targetArray remains on the stack
+        ch << DUP
+        mkExpr(i, ch)
+        mkExpr(v, ch)
+        ch << storeInstr
+        //returns targetArray
+
       case a @ FiniteArray(es) =>
         ch << Ldc(es.size)
         val storeInstr = a.getType match {

src/test/resources/regression/verification/purescala/valid/ArrayUpdated.scala

+import leon.Utils._
+
+object Test {
+
+  def test(a: Array[Int]): Int = {
+    require(a.length > 0)
+    val a2 = a.updated(0, 2)
+    a2(0)
+  } ensuring(res => res == 2)
+
+}

src/test/scala/leon/test/evaluators/EvaluatorsTests.scala

@@ -377,7 +377,12 @@ class EvaluatorsTests extends LeonTestSuite {
     val p = """|object Program {
                |  def boolArrayRead(bools : Array[Boolean], index : Int) : Boolean = bools(index)
                |
-               |  def intArrayRead(bools : Array[Int], index : Int) : Int = bools(index)
+               |  def intArrayRead(ints : Array[Int], index : Int) : Int = ints(index)
+               |
+               |  def intArrayUpdate(ints : Array[Int], index : Int, value: Int) : Int = {
+               |    val na = ints.updated(index, value)
+               |    na(index)
+               |  }
                |}
                |""".stripMargin
 
@@ -394,6 +399,9 @@ class EvaluatorsTests extends LeonTestSuite {
       checkComp(e, mkCall("intArrayRead", ia, IL(1)), IL(42))
       checkComp(e, ArrayLength(ia), IL(3))
 
+      checkComp(e, mkCall("intArrayUpdate", ia, IL(0), IL(13)), IL(13))
+      checkComp(e, mkCall("intArrayUpdate", ia, IL(1), IL(17)), IL(17))
+
       checkError(e, mkCall("boolArrayRead", ba, IL(2)))
     }
   }