From a30186982351d91bb74cd33188fb328b3e14c22b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 11 Apr 2014 14:32:57 +0200
Subject: [PATCH] Improve test reporting in case of fatal errors
---
src/main/scala/leon/synthesis/rules/InlineHoles.scala | 2 +-
.../regression/termination/looping/Numeric3.scala | 2 +-
src/test/scala/leon/test/LeonTestSuite.scala | 11 ++++++++++-
src/test/scala/leon/test/TestSilentReporter.scala | 7 ++++++-
.../leon/test/termination/TerminationRegression.scala | 2 ++
5 files changed, 20 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index 82fb1d135..97961429f 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -58,7 +58,7 @@ case object InlineHoles extends Rule("Inline-Holes") {
}
if (usesHoles(p.phi)) {
- val pathsToCalls = new CollectorWithPaths({
+ val pathsToCalls = CollectorWithPaths({
case fi: FunctionInvocation if usesHoles(fi) => fi
}).traverse(p.phi).map(_._2)
diff --git a/src/test/resources/regression/termination/looping/Numeric3.scala b/src/test/resources/regression/termination/looping/Numeric3.scala
index e0616cc13..510d1ab5f 100644
--- a/src/test/resources/regression/termination/looping/Numeric3.scala
+++ b/src/test/resources/regression/termination/looping/Numeric3.scala
@@ -1,4 +1,4 @@
-import leon.Utils._
+import leon.lang._
object Numeric3 {
def looping(x: Int) : Int = if (x > 0) looping(x - 1) else looping(5)
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index 9b460d584..58bd519b7 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -9,6 +9,7 @@ import scala.io.Source
import org.scalatest._
import org.scalatest.concurrent._
import org.scalatest.time.SpanSugar._
+import org.scalatest.exceptions.TestFailedException
import java.io.File
@@ -106,7 +107,15 @@ trait LeonTestSuite extends FunSuite with Timeouts {
testContext = generateContext
failAfter(5.minutes) {
- body
+ try {
+ body
+ } catch {
+ case fe: LeonFatalError =>
+ testContext.reporter match {
+ case sr: TestSilentReporter =>
+ throw new TestFailedException(sr.lastError.getOrElse("Some error"), fe, 5)
+ }
+ }
}
val total = now()-ts
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/leon/test/TestSilentReporter.scala
index ab12c9950..de20f1085 100644
--- a/src/test/scala/leon/test/TestSilentReporter.scala
+++ b/src/test/scala/leon/test/TestSilentReporter.scala
@@ -4,5 +4,10 @@ package leon
package test
class TestSilentReporter extends DefaultReporter(Settings()) {
- override def emit(msg: Message): Unit = { }
+ var lastError: Option[String] = None
+
+ override def emit(msg: Message): Unit = msg match {
+ case Message(this.ERROR, _, msg) => lastError = Some(msg.toString)
+ case _ =>
+ }
}
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 964202970..208917ec6 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -91,6 +91,7 @@ class TerminationRegression extends LeonTestSuite {
assert(reporter.warningCount === 0)
}
+ /*
forEachFileIn("unknown") { output =>
val Output(report, reporter) = output
val unknown = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("unknown") }
@@ -99,6 +100,7 @@ class TerminationRegression extends LeonTestSuite {
// assert(reporter.errorCount === 0)
assert(reporter.warningCount === 0)
}
+ */
//forEachFileIn("error", true) { output => () }
--
GitLab