Skip to content
Snippets Groups Projects
Commit 6929d665 authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Refactored testing code

parent 69c2bf47
No related branches found
No related tags found
No related merge requests found
......@@ -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)
......
......@@ -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))}")(())
}
}
}
......@@ -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")
......
......@@ -4,7 +4,7 @@ package inox
package solvers
package unrolling
class AssociativeQuantifiersSuite extends InoxTestSuite {
class AssociativeQuantifiersSuite extends TestSuite {
import inox.trees._
import dsl._
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment