From e7e27ddc8a7d5d93c7a92b85d670c7b87e392dbf Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 26 Mar 2015 18:25:51 +0100
Subject: [PATCH] Refactor tests a bit
---
src/test/scala/leon/test/LeonTestSuite.scala | 1 +
.../PureScalaVerificationRegression.scala | 12 ++++++------
.../verification/VerificationRegression.scala | 18 +++++++++---------
3 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index a5c94e9ab..8fb87c572 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -116,6 +116,7 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
case fe: LeonFatalError =>
testContext.reporter match {
case sr: TestSilentReporter =>
+ sr.lastErrors ++= fe.msg
throw new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5)
}
}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index f2bfc1374..55902fa9e 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -45,10 +45,12 @@ class PureScalaVerificationRegression extends VerificationRegression {
forEachFileIn("valid") { output =>
val Output(report, reporter) = output
- assert(report.totalConditions === report.totalValid,
- "All verification conditions ("+report.totalConditions+") should be valid.")
- assert(reporter.errorCount === 0)
- assert(reporter.warningCount === 0)
+ for (vc <- report.conditions) {
+ if (vc.value != Some(true)) {
+ fail("The following verification condition was invalid: " + vc.toString + " @" + vc.getPos)
+ }
+ }
+ reporter.terminateIfError()
}
forEachFileIn("invalid") { output =>
@@ -57,8 +59,6 @@ class PureScalaVerificationRegression extends VerificationRegression {
"There should be at least one invalid verification condition.")
assert(report.totalUnknown === 0,
"There should not be unknown verification conditions.")
- assert(reporter.errorCount >= report.totalInvalid)
- assert(reporter.warningCount === 0)
}
}
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index fdef26091..286fa774d 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -31,21 +31,23 @@ trait VerificationRegression extends LeonTestSuite {
val pipeFront: Pipeline[Program, Program]
val pipeBack : Pipeline[Program, VerificationReport]
- private def mkTest(files: List[String], leonOptions : Seq[String])(block: Output=>Unit) = {
+ private def mkTest(files: List[String])(block: Output=>Unit) = {
val extraction =
ExtractionPhase andThen
PreprocessingPhase andThen
pipeFront
- val ast = extraction.run(createLeonContext((files ++ leonOptions):_*))(files)
+ 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; displayName = p.id.name) test(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}") {
- val ctx = createLeonContext(leonOptions:_*)
- val report = pipeBack.run(ctx)(p)
- block(Output(report, ctx.reporter))
+ 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))
+ }
}
}
@@ -59,9 +61,7 @@ trait VerificationRegression extends LeonTestSuite {
val files = fs map { _.getPath }
- for (options <- optionVariants) {
- mkTest(files, options)(block)
- }
+ mkTest(files)(block)
}
--
GitLab