From c9000256d880b5181785da128332d4eb19a8c51a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 23 Sep 2013 13:47:51 +0200
Subject: [PATCH] Relax the way we report slow tests. Enforce types on set
operations
---
src/main/scala/leon/purescala/Trees.scala | 12 +++++++++---
src/test/scala/leon/test/LeonTestSuite.scala | 4 +++-
2 files changed, 12 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index ad8330622..4cf4d8bbf 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -478,9 +478,15 @@ object Trees {
case class SubsetOf(set1: Expr, set2: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- case class SetIntersection(set1: Expr, set2: Expr) extends Expr
- case class SetUnion(set1: Expr, set2: Expr) extends Expr
- case class SetDifference(set1: Expr, set2: Expr) extends Expr
+ case class SetIntersection(set1: Expr, set2: Expr) extends Expr {
+ leastUpperBound(Seq(set1, set2).map(_.getType)).foreach(setType _)
+ }
+ case class SetUnion(set1: Expr, set2: Expr) extends Expr {
+ leastUpperBound(Seq(set1, set2).map(_.getType)).foreach(setType _)
+ }
+ case class SetDifference(set1: Expr, set2: Expr) extends Expr {
+ leastUpperBound(Seq(set1, set2).map(_.getType)).foreach(setType _)
+ }
case class SetMin(set: Expr) extends Expr
case class SetMax(set: Expr) extends Expr
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index 1954187b8..415832a00 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -96,8 +96,10 @@ trait LeonTestSuite extends FunSuite with Timeouts {
}
override def test(name: String, tags: Tag*)(body: => Unit) {
+
super.test(name, tags: _*) {
val id = testIdentifier(name)
+
val ts = now()
testContext = generateContext
@@ -111,7 +113,7 @@ trait LeonTestSuite extends FunSuite with Timeouts {
val stats = getStats(id)
if (!stats.accountsFor(total)) {
- fail("Test took too long to run: "+total+"ms (avg: "+stats.avg+", stddev: "+stats.stddev+")")
+ info(Console.YELLOW+"[warning] Test took too long to run: "+total+"ms (avg: "+stats.avg+", stddev: "+stats.stddev+")")
}
storeStats(id, stats.withValue(total))
--
GitLab