From ffc61460a5c0a4f4126e319b25e6c4e1b597bab3 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 23 Dec 2015 01:38:12 +0100
Subject: [PATCH] Fix verification sub-suite for GenC
---
src/test/scala/leon/genc/GenCSuite.scala | 21 +++++++++++--------
.../verification/VerificationSuite.scala | 4 ++--
.../verification/XLangVerificationSuite.scala | 2 +-
3 files changed, 15 insertions(+), 12 deletions(-)
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
index d9fe551bf..a8e0368ee 100644
--- a/src/test/scala/leon/genc/GenCSuite.scala
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -180,20 +180,23 @@ class GenCSuite extends LeonRegressionSuite {
}
}
- protected def verifyValidTests() = {
- class AltVerificationSuite(override val testDir: String) extends XLangVerificationSuite {
- def run() = testValid() // Test only the valid ones
- }
+ class AltVerificationSuite(override val testDir: String) extends XLangVerificationSuite {
+ override def testAll() = testValid() // Test only the valid ones
- // Use our test dir and not the one from XLangVerificationSuite
- val verifier = new AltVerificationSuite(testDir)
+ override def suiteName = "Verification Suite For GenC"
- test("verifying test cases") { verifier.run() }
+ // Add a timeout for the verification
+ override def optionVariants =
+ super.optionVariants map { opts => "--timeout=5" :: opts }
}
- protected def testAll() = {
- verifyValidTests()
+ // Run verification suite as a nested suite
+ override def nestedSuites = {
+ // Use our test dir and not the one from XLangVerificationSuite
+ scala.collection.immutable.IndexedSeq(new AltVerificationSuite(testDir))
+ }
+ protected def testAll() = {
// Set C compiler according to the platform we're currently running on
detectCompiler match {
case Some(cc) => testValid(cc)
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index b23fb0c4e..d7eafb38c 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -19,7 +19,7 @@ import org.scalatest.{Reporter => _, _}
// This is because we compile all tests from each folder together.
trait VerificationSuite extends LeonRegressionSuite {
- val optionVariants: List[List[String]]
+ def optionVariants: List[List[String]]
val testDir: String
val ignored: Seq[String] = Seq()
@@ -81,7 +81,7 @@ trait VerificationSuite extends LeonRegressionSuite {
private[verification] def forEachFileIn(cat: String)(block: Output => Unit) {
val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
- fs foreach { file =>
+ fs foreach { file =>
assert(file.exists && file.isFile && file.canRead,
s"Benchmark ${file.getName} is not a readable file")
}
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 0136b7b06..0b6a0c37d 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -9,7 +9,7 @@ import leon.solvers.SolverFactory
// This is because we compile all tests from each folder together.
class XLangVerificationSuite extends VerificationSuite {
- val optionVariants: List[List[String]] = {
+ def optionVariants: List[List[String]] = {
val isZ3Available = SolverFactory.hasZ3
List(
--
GitLab