From 20291961ff530f28cd3f01da7cdcfff4e089dfa6 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 29 Sep 2015 19:26:24 +0200
Subject: [PATCH] Fix VerificationSuite
Fix how names are printed
Fix how tests are ignored
Ignore correct tests
---
.../termination/TerminationSuite.scala | 1 +
.../PureScalaVerificationSuite.scala | 6 ++++++
.../verification/VerificationSuite.scala | 16 +++++++++++++---
.../verification/XLangVerificationSuite.scala | 4 +---
4 files changed, 21 insertions(+), 6 deletions(-)
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 5be322e1d..321160563 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -34,6 +34,7 @@ class TerminationSuite extends LeonRegressionSuite {
val ignored = List(
"verification/purescala/valid/MergeSort.scala",
+ "verification/purescala/valid/Nested14.scala",
"verification/purescala/valid/InductiveQuantification.scala"
)
diff --git a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
index 541056449..d72e74f26 100644
--- a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
@@ -15,6 +15,12 @@ class PureScalaVerificationSuite extends VerificationSuite {
val testDir = "regression/verification/purescala/"
val pipeFront = xlang.NoXLangFeaturesChecking
val pipeBack = AnalysisPhase
+
+ override val ignored = Seq(
+ "verification/purescala/valid/Nested15.scala",
+ "verification/purescala/invalid/Nested15.scala"
+ )
+
val optionVariants: List[List[String]] = {
val isZ3Available = try {
Z3Interpreter.buildDefault.free()
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 4bf89cee8..63bf613d1 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -19,6 +19,8 @@ trait VerificationSuite extends LeonRegressionSuite {
val optionVariants: List[List[String]]
val testDir: String
+ val ignored: Seq[String] = Seq()
+
private var counter: Int = 0
private def nextInt(): Int = {
counter += 1
@@ -42,11 +44,19 @@ trait VerificationSuite extends LeonRegressionSuite {
val (ctx2, ast) = extraction.run(ctx, files)
val programs = {
val (user, lib) = ast.units partition { _.isMainUnit }
- user map { u => (u.id, Program(u :: lib)) }
+ user map ( u => Program(u :: lib) )
}
- for ((id, p) <- programs; options <- optionVariants) {
+ for ( p <- programs; options <- optionVariants) {
+
+ val displayName = s"$cat/${p.units.head.id.name}.scala"
+
val index = nextInt()
- test(f"$index%3d: ${id.name} ${options.mkString(" ")}") {
+ val ts = if (ignored exists (_.endsWith(displayName)))
+ ignore _
+ else
+ test _
+
+ ts(f"$index%3d: $displayName ${options.mkString(" ")}", Seq()) {
val ctx = createLeonContext(options: _*)
if (forError) {
intercept[LeonFatalError] {
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 83730cc76..26513352b 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -38,9 +38,7 @@ class XLangVerificationSuite extends LeonRegressionSuite {
fullName
}
- val ignored = List(
- "regression/verification/xlang/valid/Nested15.scala"
- )
+ val ignored = List()
val t = if (ignored.exists(displayName endsWith _)) {
ignore _
--
GitLab