diff --git a/library/collection/package.scala b/library/collection/package.scala
index 77d953a10a7f7c4b6562e7b7203fa90ba13ccebc..e163eaf4a70c525be71644ec0e05afeb4f63d87a 100644
--- a/library/collection/package.scala
+++ b/library/collection/package.scala
@@ -4,6 +4,7 @@ package leon
import leon.annotation._
import leon.collection.List
+import leon.lang._
import leon.lang.synthesis.choose
package object collection {
diff --git a/library/lang/Set.scala b/library/lang/Set.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dcedd1e0b06c865f8f49edab5b13d5f347181844
--- /dev/null
+++ b/library/lang/Set.scala
@@ -0,0 +1,18 @@
+package leon.lang
+import leon.annotation._
+
+object Set {
+ def empty[T] = Set[T]()
+}
+
+@ignore
+case class Set[T](elems: T*) {
+ def +(a: T): Set[T] = ???
+ def ++(a: Set[T]): Set[T] = ???
+ def -(a: T): Set[T] = ???
+ def --(a: Set[T]): Set[T] = ???
+ def contains(a: T): Boolean = ???
+ def isEmpty: Boolean = ???
+ def subsetOf(b: Set[T]): Boolean = ???
+ def &(a: Set[T]): Set[T] = ???
+}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index eac0ef94fc699d6f999250dc3d7e072fc05abe13..6fab7051bea118c4967f0cce66697d8aa7ef230d 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -26,7 +26,8 @@ trait ASTExtractors {
protected lazy val tuple4Sym = classFromName("scala.Tuple4")
protected lazy val tuple5Sym = classFromName("scala.Tuple5")
protected lazy val mapSym = classFromName("scala.collection.immutable.Map")
- protected lazy val setSym = classFromName("scala.collection.immutable.Set")
+ protected lazy val scalaSetSym = classFromName("scala.collection.immutable.Set")
+ protected lazy val setSym = classFromName("leon.lang.Set")
protected lazy val optionClassSym = classFromName("scala.Option")
protected lazy val arraySym = classFromName("scala.Array")
protected lazy val someClassSym = classFromName("scala.Some")
@@ -56,15 +57,19 @@ trait ASTExtractors {
}
}
- def isSetTraitSym(sym : Symbol) : Boolean = {
+ def isSetSym(sym: Symbol) : Boolean = {
getResolvedTypeSym(sym) == setSym
}
- def isMapTraitSym(sym : Symbol) : Boolean = {
+ def isScalaSetSym(sym: Symbol) : Boolean = {
+ getResolvedTypeSym(sym) == scalaSetSym
+ }
+
+ def isMapTraitSym(sym: Symbol) : Boolean = {
getResolvedTypeSym(sym) == mapSym
}
- def isMultisetTraitSym(sym : Symbol) : Boolean = {
+ def isMultisetTraitSym(sym: Symbol) : Boolean = {
sym == multisetTraitSym
}
@@ -323,8 +328,9 @@ trait ASTExtractors {
}
object ExCaseClassSyntheticJunk {
- def unapply(cd: ClassDef): Boolean = cd match {
+ def unapply(cd: Tree): Boolean = cd match {
case ClassDef(_, _, _, _) if cd.symbol.isSynthetic => true
+ case DefDef(_, _, _, _, _, _) if cd.symbol.isSynthetic && (cd.symbol.isCase || cd.symbol.isPrivate) => true
case _ => false
}
}
@@ -815,23 +821,6 @@ trait ASTExtractors {
}
}
- object ExEmptySet {
- def unapply(tree: TypeApply): Option[Tree] = tree match {
- case TypeApply(
- Select(
- Select(
- Select(
- Select(Ident(s), collectionName),
- immutableName),
- setName),
- emptyName), theTypeTree :: Nil) if (
- collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && emptyName.toString == "empty"
- ) => Some(theTypeTree)
- case TypeApply(Select(Select(Select(This(scalaName), predefName), setname), applyName), theTypeTree :: Nil) if ("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString) && "empty".equals(applyName.toString)) => Some(theTypeTree)
- case _ => None
- }
- }
-
object ExEmptyMultiset {
def unapply(tree: TypeApply): Option[Tree] = tree match {
case TypeApply(
@@ -867,14 +856,6 @@ trait ASTExtractors {
}
}
- object ExFiniteSet {
- def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
- case Apply(TypeApply(Select(Select(Select(Select(Ident(s), collectionName), immutableName), setName), applyName), theTypeTree :: Nil), args) if (collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && applyName.toString == "apply") => Some((theTypeTree, args))
- case Apply(TypeApply(Select(Select(Select(This(scalaName), predefName), setName), applyName), theTypeTree :: Nil), args) if ("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString) && setName.toString == "Set" && "apply".equals(applyName.toString)) => Some((theTypeTree, args))
- case _ => None
- }
- }
-
object ExFiniteMultiset {
def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
case Apply(
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index b4f2a020067473d80cc24274146bcf87d6b6549a..70a0eacf23b1a2d4d3e17e254422a69fcbff1d41 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -869,6 +869,7 @@ trait CodeExtraction extends ASTExtractors {
case ExFieldAccessorFunction() =>
case d if isIgnored(d.symbol) || (d.symbol.isImplicit && d.symbol.isSynthetic) =>
case tree =>
+ println(tree)
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
}
@@ -1410,8 +1411,10 @@ trait CodeExtraction extends ASTExtractors {
case ExCaseClassConstruction(tpt, args) =>
extractType(tpt) match {
case cct: CaseClassType =>
- val nargs = args.map(extractTree)
- CaseClass(cct, nargs)
+ CaseClass(cct, args.map(extractTree))
+
+ case SetType(underlying) =>
+ finiteSet(args.map(extractTree).toSet, underlying)
case _ =>
outOfSubsetError(tr, "Construction of a non-case class.")
@@ -1460,13 +1463,6 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Invalid comparison: (_: "+rt+") == (_: "+lt+")")
}
- case ExFiniteSet(tt, args) =>
- val underlying = extractType(tt)
- finiteSet(args.map(extractTree).toSet, underlying)
- case ExEmptySet(tt) =>
- val underlying = extractType(tt)
- EmptySet(underlying)
-
case ExFiniteMultiset(tt, args) =>
val underlying = extractType(tt)
finiteMultiset(args.map(extractTree),underlying)
@@ -1689,11 +1685,11 @@ trait CodeExtraction extends ASTExtractors {
or(a1, a2)
// Set methods
- case (IsTyped(a1, SetType(b1)), "min", Nil) =>
- SetMin(a1)
+ //case (IsTyped(a1, SetType(b1)), "min", Nil) =>
+ // SetMin(a1)
- case (IsTyped(a1, SetType(b1)), "max", Nil) =>
- SetMax(a1)
+ //case (IsTyped(a1, SetType(b1)), "max", Nil) =>
+ // SetMax(a1)
case (IsTyped(a1, SetType(b1)), "++", List(IsTyped(a2, SetType(b2)))) if b1 == b2 =>
SetUnion(a1, a2)
@@ -1710,6 +1706,9 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, SetType(b1)), "contains", List(a2)) =>
ElementOfSet(a2, a1)
+ case (IsTyped(a1, SetType(b1)), "isEmpty", List()) =>
+ Equals(a1, finiteSet(Set(), b1))
+
// Multiset methods
case (IsTyped(a1, MultisetType(b1)), "++", List(IsTyped(a2, MultisetType(b2)))) if b1 == b2 =>
MultisetUnion(a1, a2)
@@ -1795,7 +1794,10 @@ trait CodeExtraction extends ASTExtractors {
case TypeRef(_, sym, _) if isBigIntSym(sym) =>
IntegerType
- case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) =>
+ case TypeRef(_, sym, btt :: Nil) if isScalaSetSym(sym) =>
+ outOfSubsetError(pos, "Scala's Set API is no longer extracted. Make sure you import leon.lang.Set that defines supported Set operations.")
+
+ case TypeRef(_, sym, btt :: Nil) if isSetSym(sym) =>
SetType(extractType(btt))
case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) =>
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 005138c93e2fcff2a5b3994828c30601c0be52a6..a08f55c6c272fabecad5969db11850b85c7f3138 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -36,10 +36,11 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
"make sure to set the ECLIPSE_HOME environment variable to your Eclipse installation home directory"
))
- settings.classpath.value = scalaLib
- settings.usejavacp.value = false
- settings.Yrangepos.value = true
- settings.skip.value = List("patmat")
+ settings.classpath.value = scalaLib
+ settings.usejavacp.value = false
+ settings.deprecation.value = true
+ settings.Yrangepos.value = true
+ settings.skip.value = List("patmat")
val compilerOpts = Build.libFiles ::: args.filterNot(_.startsWith("--"))
diff --git a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
index 60be71545731d2db588250e49a6536e0314946a6..d04cebb3e04eaa78a555c33f1093c1a1e6935849 100644
--- a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
+++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
@@ -53,28 +53,14 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
case _ =>
val buf = new StringBuilder(msg)
val lpos = LeonOffsetPosition(pos.line, pos.column, pos.point, pos.source.file.file)
- printMessage(msg+"\n"+getSourceLine(pos), lpos, severity)
+ printMessage(msg, lpos, severity)
}
}
+
def print(pos: Position, msg: String, severity: Severity) {
printMessage(pos, clabel(severity) + msg, severity)
}
- def getSourceLine(pos: Position) = {
- pos.lineContent.stripLineEnd+getColumnMarker(pos)
- }
-
- def getColumnMarker(pos: Position) = if (pos.isDefined) {
- "\n"+(" " * (pos.column - 1) + "^")
- } else {
- ""
- }
-
- def printSummary() {
- if (WARNING.count > 0) printMessage(getCountString(WARNING) + " found", LeonNoPosition, INFO)
- if ( ERROR.count > 0) printMessage(getCountString(ERROR ) + " found", LeonNoPosition, INFO)
- }
-
def display(pos: Position, msg: String, severity: Severity) {
severity.count += 1
if (severity != ERROR || severity.count <= ERROR_LIMIT)
diff --git a/src/test/resources/regression/repair/Heap4.scala b/src/test/resources/regression/repair/Heap4.scala
index cd06242701790e72236f57604db4ec8c83919b97..75f03aab55f773210738e0455d8e0468a33b03cb 100644
--- a/src/test/resources/regression/repair/Heap4.scala
+++ b/src/test/resources/regression/repair/Heap4.scala
@@ -4,8 +4,9 @@
* Date: 20.11.2013
**/
+import leon._
+import leon.lang._
import leon.collection._
-import leon._
object HeapSort {
diff --git a/src/test/resources/regression/repair/MergeSort2.scala b/src/test/resources/regression/repair/MergeSort2.scala
index 2cb780bb058d36a4b4b2627d682b56504ba8e024..ca22569d80c779b3fce3575b66ae0fd701661062 100644
--- a/src/test/resources/regression/repair/MergeSort2.scala
+++ b/src/test/resources/regression/repair/MergeSort2.scala
@@ -1,5 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.lang._
import leon.collection._
object MergeSort {
diff --git a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
index 5c2f48c3d444fec728c3c4817957518b2fe60c7c..c758798bf753fc5ac5f1f1a9c65927e509166b8c 100644
--- a/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
+++ b/src/test/resources/regression/termination/valid/BinaryTreeImp.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/termination/valid/ListWithSize.scala b/src/test/resources/regression/termination/valid/ListWithSize.scala
index 00bd968ad51692c9617098d3315b94d85c5456a9..af8aafeb8d5f669f8daf7fbc9b8c3abc69fd6f3e 100644
--- a/src/test/resources/regression/termination/valid/ListWithSize.scala
+++ b/src/test/resources/regression/termination/valid/ListWithSize.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/termination/valid/QuickSort.scala b/src/test/resources/regression/termination/valid/QuickSort.scala
index 5687c778f47ee1d1084441a009f4bdf67bbbcccf..e356bdc2a2b8a1c412e90a3033ae269faf6d7df0 100644
--- a/src/test/resources/regression/termination/valid/QuickSort.scala
+++ b/src/test/resources/regression/termination/valid/QuickSort.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
+import leon.lang._
object QuickSort {
sealed abstract class List
diff --git a/src/test/resources/regression/termination/valid/RedBlackTree.scala b/src/test/resources/regression/termination/valid/RedBlackTree.scala
index 76c4e03a99774859ccb4238c8d91093fc1cf256d..2d48a25e0dee87ac6f94563e3b28cb48ca8eb567 100644
--- a/src/test/resources/regression/termination/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/termination/valid/RedBlackTree.scala
@@ -1,7 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
-//import scala.collection.immutable.Multiset
+import leon.lang._
object RedBlackTree {
sealed abstract class Color
diff --git a/src/test/resources/regression/termination/valid/SimpInterpret.scala b/src/test/resources/regression/termination/valid/SimpInterpret.scala
index 22c31f1944198e0d5795dfbde575fc660492e4e4..76fcd4145509440741b521bf26fa97dcc9af2dd9 100644
--- a/src/test/resources/regression/termination/valid/SimpInterpret.scala
+++ b/src/test/resources/regression/termination/valid/SimpInterpret.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-//import scala.collection.immutable.Set
//import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
index 1f74ed4b12933352dedeb22dadff0f1d1121f19d..0b55b9a5164bbd86e8be0bc4a61e8f5f29867d88 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala b/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
index a62a765f5eb3700b90be8fea45df8812413f1b43..ad22edcd88daeb11f1b1d41f35dc48e5766ad0ad 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
index a3120a9bc9e728ab5a6f352d649b64e9c67e761c..81109ba330f13246061e7ef9cb1422ab72223ab9 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
index 2986a4342ac0bf5f65b2bb21dad5324fdb5223b8..3965ab57d9021ef7b9823d702d83daa14728b80f 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
index a41dab8262f9910662a994b0d6def78bf1bac5c7..4c2beb4c78bbcbe3177249b9866d6df73fa65bb6 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala b/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
index 841befb415c77e3609b9ad7bf28a1e760d3ce39f..edaee5e92a4d10eb089e6e9a91e3e27678d4f84a 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
index bd0596fbaab48f4a64309e71d019db53ed72db2a..87076bb973026c4eac73fe191bc80d778105b30c 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
index 5b4d876143454ef9e35de903fd5634df0663829f..d82f045b52c4870e0d243fd77777e1e19a5b60bd 100644
--- a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
index 7c880d29975fe35814606bcd8ddfeb97319d31e7..46e90ccfc64fc33383abcfac5db86e7060821b6e 100644
--- a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index 6cf45fb74e6944c025ffcfc73992caead6bee1d4..547978dbcca900272b76aac30dfd8e2a8f9e2c62 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
index c37713f8e5f91aa9d593520d37060697aa6d58e8..f56a174de585e0e17ee64ae989af8cbee56b4371 100644
--- a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
index 7486b49f3b3b40074fac773a36dca29eb9adb322..006fbde9ac76dd8f366fd0f495fe4f349b861eaf 100644
--- a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
index 5fd977e8b3c8b76662e5e4aa004d91af68962242..39cc5b7326c3d1aa964055f6335336943b2afcf7 100644
--- a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index 4e0d60a94973dda4f56f8853cc076efa3c907588..7c89f364600e95edb8c0f266cb5e22f65d1adbea 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
index 341c3ec8592bc4e7050d1187bf8d9f2363b68f3c..72a27c049c546696d8dd3853fe0ccdd26e077082 100644
--- a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
index 2ca4e27fdc6623ef009483e69c72a099016ec3f2..66e3f84ecfa11a460c6e721f69cb44d51def285e 100644
--- a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
index 12cfc679ee3219d1af89d306b414b506ed2415be..e24935bbedb8f87e0778f29f44f3a4758560fc11 100644
--- a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
index f66557f0da7448cc3aa5dc292dc31a24ab853d26..882dfa14001698091f09b51c67e346d1a74480b0 100644
--- a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala b/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala
index 35bae37259c9d1b12606521846e9d5f3ca9154ac..c7e8bd533ed8e7b49301a903b79939810884a5f7 100644
--- a/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala
@@ -1,5 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.lang._
+
object Subtyping1 {
sealed abstract class Tree
diff --git a/src/test/resources/regression/verification/xlang/invalid/Mean.scala b/src/test/resources/regression/verification/xlang/invalid/Mean.scala
index 9d1fd563c3cc8c9bf191aeeef5e1be093e78bd32..02240e73b2e04244e8a55c1881e21b0381852302 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Mean.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Mean.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/xlang/valid/Mean.scala b/src/test/resources/regression/verification/xlang/valid/Mean.scala
index 16e032896c0b9134cd44be59d1f23b0e2b46e0c7..155b7095a112266b76fed38b3037e9412a0fa49e 100644
--- a/src/test/resources/regression/verification/xlang/valid/Mean.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Mean.scala
@@ -1,6 +1,5 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index 0c8f08b70a16bd9ca56c04902f716be209586329..c43e597a61aced0c3a4708d0c9189ee8c91a7ab0 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -103,7 +103,6 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
}
override def test(name: String, tags: Tag*)(body: => Unit) {
-
super.test(name, tags: _*) {
val id = testIdentifier(name)
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index 9142374f72e9a3fb7cbc3eabc0fc9d48e0c8ca9f..88f1481f7504446530f5eee853ab6fe3e6bb5dce 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -127,7 +127,8 @@ class CodeGenTests extends test.LeonTestSuite {
val code = """
-
+ import leon.lang._
+
object simple {
abstract class Abs
case class Conc(x : Int) extends Abs
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 87d5a2d078393bd4089054c63df2ed87d76778f2..81eee7077af71761f1b5d4121bba6ac33a759219 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -298,7 +298,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
test("Sets") {
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| sealed abstract class List
| case class Nil() extends List
| case class Cons(head : Int, tail : List) extends List
@@ -343,20 +344,21 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
test("Maps") {
- val p = """|object Program {
- |sealed abstract class PList
- |case class PNil() extends PList
- |case class PCons(headfst : Int, headsnd : Int, tail : PList) extends PList
+ val p = """|import leon.lang._
+ |object Program {
+ | sealed abstract class PList
+ | case class PNil() extends PList
+ | case class PCons(headfst : Int, headsnd : Int, tail : PList) extends PList
|
- |def toMap(pl : PList) : Map[Int,Int] = pl match {
- | case PNil() => Map.empty[Int,Int]
- | case PCons(f,s,xs) => toMap(xs).updated(f, s)
- |}
+ | def toMap(pl : PList) : Map[Int,Int] = pl match {
+ | case PNil() => Map.empty[Int,Int]
+ | case PCons(f,s,xs) => toMap(xs).updated(f, s)
+ | }
|
- |def finite0() : Map[Int,Int] = Map[Int, Int]()
- |def finite1() : Map[Int,Int] = Map(1 -> 2)
- |def finite2() : Map[Int,Int] = Map(2 -> 3, 1 -> 2)
- |def finite3() : Map[Int,Int] = finite1().updated(2, 3)
+ | def finite0() : Map[Int,Int] = Map[Int, Int]()
+ | def finite1() : Map[Int,Int] = Map(1 -> 2)
+ | def finite2() : Map[Int,Int] = Map(2 -> 3, 1 -> 2)
+ | def finite3() : Map[Int,Int] = finite1().updated(2, 3)
|}""".stripMargin
implicit val prog = parseString(p)
@@ -377,7 +379,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
test("Arrays") {
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| def boolArrayRead(bools : Array[Boolean], index : Int) : Boolean = bools(index)
|
| def intArrayRead(ints : Array[Int], index : Int) : Int = ints(index)
@@ -410,7 +413,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
test("Sets and maps of structures") {
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| case class MyPair(x : Int, y : Boolean)
|
| def buildPairCC(x : Int, y : Boolean) : MyPair = MyPair(x,y)
@@ -432,7 +436,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
test("Executing Chooses") {
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| import leon.lang._
| import leon.lang.synthesis._
|
@@ -451,7 +456,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
test("Infinite Recursion") {
import leon.codegen._
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| import leon.lang._
|
| def c(i : Int) : Int = c(i-1)
@@ -467,7 +473,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
test("Wrong Contracts") {
import leon.codegen._
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| import leon.lang._
|
| def c(i : Int) : Int = {
@@ -484,7 +491,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
test("Pattern Matching") {
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| abstract class List;
| case class Cons(h: Int, t: List) extends List;
| case object Nil extends List;
diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala
index 2a287efd2bf956ca1a36f518a2b41001d7f2e4dc..558621bb2e15e1504f83d48c389423e24c24ee25 100644
--- a/src/test/scala/leon/test/verification/NewSolversRegression.scala
+++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala
@@ -42,7 +42,4 @@ class NewSolversRegression extends VerificationRegression {
else Nil
)
}
-
- test()
-
}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index bf9256a416bb55052edfccb9b521c1b0c008263e..0221488a5886cd885e84ae175fef6dea9c76fb3d 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -46,6 +46,4 @@ class PureScalaVerificationRegression extends VerificationRegression {
)
}
- test()
-
}
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index 0f46c569ba4feec4f126cca3d251056aa473f3db..a03cfcd9704addfa859ac103d91a21cfa7542fe7 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -10,6 +10,7 @@ import leon.purescala.Definitions.Program
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
+import org.scalatest.{Reporter => TestReporter, _}
// If you add another regression test, make sure it contains one object whose name matches the file name
// This is because we compile all tests from each folder separately.
@@ -29,22 +30,36 @@ trait VerificationRegression extends LeonTestSuite {
val pipeBack : Pipeline[Program, VerificationReport]
private def mkTest(files: List[String])(block: Output=>Unit) = {
- val extraction =
+ val extraction =
ExtractionPhase andThen
PreprocessingPhase andThen
pipeFront
- val ast = extraction.run(createLeonContext(files:_*))(files)
- val programs = {
- val (user, lib) = ast.units partition { _.isMainUnit }
- user map { u => Program(u.id.freshen, u :: lib) }
- }
- for (p <- programs; options <- optionVariants) {
- test(f"${nextInt()}%3d: ${p.id.name} ${options.mkString(" ")}") {
- val ctx = createLeonContext(options: _*)
- val report = pipeBack.run(ctx)(p)
- block(Output(report, ctx.reporter))
+ val ctx = createLeonContext(files:_*)
+
+ try {
+ val ast = extraction.run(ctx)(files)
+ val programs = {
+ val (user, lib) = ast.units partition { _.isMainUnit }
+ user map { u => Program(u.id.freshen, u :: lib) }
+ }
+ for (p <- programs; options <- optionVariants) {
+ test(f"${nextInt()}%3d: ${p.id.name} ${options.mkString(" ")}") {
+ val ctx = createLeonContext(options: _*)
+ val report = pipeBack.run(ctx)(p)
+ block(Output(report, ctx.reporter))
+ }
}
+ } catch {
+ case _: LeonFatalError =>
+ ctx.reporter match {
+ case sr: TestSilentReporter =>
+ println("Unnexpected Fatal error:")
+ for (e <- sr.lastErrors) {
+ println(" "+e)
+ }
+ case _ =>
+ }
}
}
@@ -61,7 +76,7 @@ trait VerificationRegression extends LeonTestSuite {
mkTest(files)(block)
}
- def test() = {
+ override def run(testName: Option[String], args: Args): Status = {
forEachFileIn("valid") { output =>
val Output(report, reporter) = output
for ((vc, vr) <- report.vrs) {
@@ -79,5 +94,7 @@ trait VerificationRegression extends LeonTestSuite {
assert(report.totalUnknown === 0,
"There should not be unknown verification conditions.")
}
+
+ super.run(testName, args)
}
}