Support for literal arrays

src/main/scala/leon/plugin/CodeExtraction.scala

@@ -310,8 +310,8 @@ trait CodeExtraction extends Extractors {
       throw new ImpureCodeEncounteredException(null)
     }
     def unsupported(tr: Tree, msg: String): Nothing = {
-      reporter.error(tr.pos, tr.toString)
       reporter.error(tr.pos, msg)
+      reporter.error(tr.pos, tr.toString)
       throw new ImpureCodeEncounteredException(tr)
     }
 
@@ -390,15 +390,18 @@ trait CodeExtraction extends Extractors {
       var rest = tmpRest
 
       val res = current match {
+        case ExArrayLiteral(tpe, args) =>
+          FiniteArray(args.map(extractTree)).setType(ArrayType(extractType(tpe)))
+
         case ExCaseObject(sym) =>
           classesToClasses.get(sym) match {
             case Some(ccd: CaseClassDef) =>
               CaseClass(ccd, Seq())
-
             case _ =>
-              unsupported(tr, "Unknown case class "+sym.name)
+              unsupported(tr, "Unknown case object "+sym.name)
           }
 
+
         case ExParameterlessMethodCall(t,n) if extractTree(t).getType.isInstanceOf[CaseClassType] =>
           val selector = extractTree(t)
           val selType = selector.getType

src/main/scala/leon/plugin/Extractors.scala

@@ -310,6 +310,23 @@ trait Extractors {
       }
     }
 
+    object ExArrayLiteral {
+      def unapply(tree: Apply): Option[(Type, Seq[Tree])] = tree match {
+        case Apply(ExSelected("scala", "Array", "apply"), args) =>
+          tree.tpe match {
+            case TypeRef(_, _, List(t1)) =>
+              Some((t1, args))
+            case _ =>
+              None
+          }
+        case Apply(Apply(TypeApply(ExSelected("scala", "Array", "apply"), List(tpt)), args), ctags) =>
+          Some((tpt.tpe, args))
+
+        case _ =>
+          None
+      }
+    }
+
     object ExTuple {
       def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
         case Apply(

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

+import leon.Utils._
+object Numerals {
+  def foo(): Int = {
+    val b : Array[Int] = Array[Int](1,2,3)
+    val a : Array[Int] = Array(1,2,3)
+    a.length
+  } ensuring { _ > 0 }
+}