From a86f13a1647d1afad71fff2d8392a226ef217be8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 17 Apr 2015 17:44:06 +0200
Subject: [PATCH] Leon defines its own Sets
---
library/collection/package.scala | 1 +
library/lang/Set.scala | 18 ++++++++
.../leon/frontends/scalac/ASTExtractors.scala | 41 +++++------------
.../frontends/scalac/CodeExtraction.scala | 30 ++++++------
.../frontends/scalac/ExtractionPhase.scala | 9 ++--
.../frontends/scalac/SimpleReporter.scala | 18 +-------
.../resources/regression/repair/Heap4.scala | 3 +-
.../regression/repair/MergeSort2.scala | 1 +
.../termination/valid/BinaryTreeImp.scala | 1 -
.../termination/valid/ListWithSize.scala | 1 -
.../termination/valid/QuickSort.scala | 2 +-
.../termination/valid/RedBlackTree.scala | 3 +-
.../termination/valid/SimpInterpret.scala | 1 -
.../newsolvers/valid/AmortizedQueue.scala | 1 -
.../newsolvers/valid/AssociativeList.scala | 1 -
.../newsolvers/valid/InsertionSort.scala | 1 -
.../newsolvers/valid/ListOperations.scala | 1 -
.../newsolvers/valid/PropositionalLogic.scala | 1 -
.../newsolvers/valid/RedBlackTree.scala | 1 -
.../newsolvers/valid/SearchLinkedList.scala | 1 -
.../purescala/invalid/InsertionSort.scala | 1 -
.../purescala/invalid/ListOperations.scala | 1 -
.../invalid/PropositionalLogic.scala | 1 -
.../purescala/invalid/RedBlackTree.scala | 1 -
.../purescala/valid/AmortizedQueue.scala | 1 -
.../purescala/valid/AssociativeList.scala | 1 -
.../purescala/valid/InsertionSort.scala | 1 -
.../purescala/valid/ListOperations.scala | 1 -
.../purescala/valid/PropositionalLogic.scala | 1 -
.../purescala/valid/RedBlackTree.scala | 1 -
.../purescala/valid/SearchLinkedList.scala | 1 -
.../purescala/valid/Subtyping1.scala | 2 +
.../verification/xlang/invalid/Mean.scala | 1 -
.../verification/xlang/valid/Mean.scala | 1 -
src/test/scala/leon/test/LeonTestSuite.scala | 1 -
.../leon/test/codegen/CodeGenTests.scala | 3 +-
.../test/evaluators/EvaluatorsTests.scala | 46 +++++++++++--------
.../verification/NewSolversRegression.scala | 3 --
.../PureScalaVerificationRegression.scala | 2 -
.../verification/VerificationRegression.scala | 41 ++++++++++++-----
40 files changed, 118 insertions(+), 129 deletions(-)
create mode 100644 library/lang/Set.scala
diff --git a/library/collection/package.scala b/library/collection/package.scala
index 77d953a10..e163eaf4a 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 000000000..dcedd1e0b
--- /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 eac0ef94f..6fab7051b 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 b4f2a0200..70a0eacf2 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 005138c93..a08f55c6c 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 60be71545..d04cebb3e 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 cd0624270..75f03aab5 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 2cb780bb0..ca22569d8 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 5c2f48c3d..c758798bf 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 00bd968ad..af8aafeb8 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 5687c778f..e356bdc2a 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 76c4e03a9..2d48a25e0 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 22c31f194..76fcd4145 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 1f74ed4b1..0b55b9a51 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 a62a765f5..ad22edcd8 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 a3120a9bc..81109ba33 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 2986a4342..3965ab57d 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 a41dab826..4c2beb4c7 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 841befb41..edaee5e92 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 bd0596fba..87076bb97 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 5b4d87614..d82f045b5 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 7c880d299..46e90ccfc 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 6cf45fb74..547978dbc 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 c37713f8e..f56a174de 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 7486b49f3..006fbde9a 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 5fd977e8b..39cc5b732 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 4e0d60a94..7c89f3646 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 341c3ec85..72a27c049 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 2ca4e27fd..66e3f84ec 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 12cfc679e..e24935bbe 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 f66557f0d..882dfa140 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 35bae3725..c7e8bd533 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 9d1fd563c..02240e73b 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 16e032896..155b7095a 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 0c8f08b70..c43e597a6 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 9142374f7..88f1481f7 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 87d5a2d07..81eee7077 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 2a287efd2..558621bb2 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 bf9256a41..0221488a5 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 0f46c569b..a03cfcd97 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)
}
}
--
GitLab