From 710769d2ef0fa9e48a8ec2c6cd99af6b3e217fc0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 8 Oct 2013 19:12:07 +0200
Subject: [PATCH] Support for literal arrays
---
src/main/scala/leon/plugin/CodeExtraction.scala | 9 ++++++---
src/main/scala/leon/plugin/Extractors.scala | 17 +++++++++++++++++
.../purescala/valid/ArrayLiterals.scala | 8 ++++++++
3 files changed, 31 insertions(+), 3 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 6f9c3101d..dd71afeec 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/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
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 00da888f6..8735654d7 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/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(
diff --git a/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala b/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
new file mode 100644
index 000000000..2ce0669e6
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ArrayLiterals.scala
@@ -0,0 +1,8 @@
+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 }
+}
--
GitLab