From 6929d6654d15cfc3f6edede228064edc96770a9b Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 24 Oct 2016 18:15:01 +0200
Subject: [PATCH] Refactored testing code
---
src/it/scala/inox/ResourceUtils.scala | 2 --
.../{InoxTestSuite.scala => TestSuite.scala} | 21 ++++++++++++-------
.../scala/inox/solvers/SolvingTestSuite.scala | 2 +-
.../AssociativeQuantifiersSuite.scala | 2 +-
4 files changed, 15 insertions(+), 12 deletions(-)
rename src/it/scala/inox/{InoxTestSuite.scala => TestSuite.scala} (50%)
diff --git a/src/it/scala/inox/ResourceUtils.scala b/src/it/scala/inox/ResourceUtils.scala
index c43039166..3c8a910b6 100644
--- a/src/it/scala/inox/ResourceUtils.scala
+++ b/src/it/scala/inox/ResourceUtils.scala
@@ -11,8 +11,6 @@ import utils._
trait ResourceUtils {
- val resourcesDir = "src/it/resources"
-
def resourceFiles(dir: String, filter: String => Boolean = (s: String) => true, recursive: Boolean = false): Seq[File] = {
Option(getClass.getResource(s"/$dir")).toSeq.flatMap { url =>
val baseDir = new File(url.getPath)
diff --git a/src/it/scala/inox/InoxTestSuite.scala b/src/it/scala/inox/TestSuite.scala
similarity index 50%
rename from src/it/scala/inox/InoxTestSuite.scala
rename to src/it/scala/inox/TestSuite.scala
index d94fcca60..229e55c40 100644
--- a/src/it/scala/inox/InoxTestSuite.scala
+++ b/src/it/scala/inox/TestSuite.scala
@@ -7,15 +7,18 @@ import org.scalatest.concurrent._
import utils._
-trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
+trait TestSuite extends FunSuite with Matchers with Timeouts {
val configurations: Seq[Seq[OptionValue[_]]] = Seq(Seq.empty)
- private def optionsString(options: Options): String = {
- "solver=" + options.findOptionOrDefault(optSelectedSolvers).head + " " +
- "feelinglucky=" + options.findOptionOrDefault(solvers.unrolling.optFeelingLucky) + " " +
- "checkmodels=" + options.findOptionOrDefault(solvers.optCheckModels) + " " +
- "unrollassumptions=" + options.findOptionOrDefault(solvers.unrolling.optUnrollAssumptions)
+ private val counter = new UniqueCounter[Unit]
+ counter.nextGlobal // Start at 1
+
+ protected def optionsString(options: Options): String = {
+ "solvr=" + options.findOptionOrDefault(optSelectedSolvers).head + " " +
+ "lucky=" + options.findOptionOrDefault(solvers.unrolling.optFeelingLucky) + " " +
+ "check=" + options.findOptionOrDefault(solvers.optCheckModels) + " " +
+ "assum=" + options.findOptionOrDefault(solvers.unrolling.optUnrollAssumptions)
}
protected def test(name: String, tags: Tag*)(body: Context => Unit): Unit = {
@@ -23,7 +26,8 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
val reporter = new TestSilentReporter
val ctx = Context(reporter, new InterruptManager(reporter), Options(config))
try {
- super.test(name + " " + optionsString(ctx.options))(body(ctx))
+ val index = counter.nextGlobal
+ super.test(f"$index%3d: $name ${optionsString(ctx.options)}")(body(ctx))
} catch {
case err: FatalError =>
reporter.lastErrors :+= err.msg
@@ -34,7 +38,8 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts {
protected def ignore(name: String, tags: Tag*)(body: Context => Unit): Unit = {
for (config <- configurations) {
- super.ignore(name + " " + optionsString(Options(config)))(())
+ val index = counter.nextGlobal
+ super.ignore(f"$index%3d: $name ${optionsString(Options(config))}")(())
}
}
}
diff --git a/src/it/scala/inox/solvers/SolvingTestSuite.scala b/src/it/scala/inox/solvers/SolvingTestSuite.scala
index 17b9c8630..2fe9c90e3 100644
--- a/src/it/scala/inox/solvers/SolvingTestSuite.scala
+++ b/src/it/scala/inox/solvers/SolvingTestSuite.scala
@@ -3,7 +3,7 @@
package inox
package solvers
-trait SolvingTestSuite extends InoxTestSuite {
+trait SolvingTestSuite extends TestSuite {
override val configurations = for {
solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
diff --git a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
index 4ebc09cb9..bb914c053 100644
--- a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala
@@ -4,7 +4,7 @@ package inox
package solvers
package unrolling
-class AssociativeQuantifiersSuite extends InoxTestSuite {
+class AssociativeQuantifiersSuite extends TestSuite {
import inox.trees._
import dsl._
--
GitLab