diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 0be138d6d679da509853bb893377291e3ca0c678..c907a66569bee4906fce477d9216afd8a278cd75 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -6,7 +6,7 @@ import leon._
import leon.test._
import leon.verification.{AnalysisPhase,VerificationReport}
-
+import leon.purescala.Definitions.Program
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
@@ -14,55 +14,14 @@ import _root_.smtlib.interpreters._
import java.io.File
-class PureScalaVerificationRegression extends LeonTestSuite {
- private var counter : Int = 0
- private def nextInt() : Int = {
- counter += 1
- counter
- }
- private case class Output(report : VerificationReport, reporter : Reporter)
-
- private def mkPipeline : Pipeline[List[String], VerificationReport] =
- ExtractionPhase andThen
- PreprocessingPhase andThen
- xlang.NoXLangFeaturesChecking andThen
- AnalysisPhase
-
- private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
- val fullName = file.getPath()
- val start = fullName.indexOf("regression")
-
- val displayName = if(start != -1) {
- fullName.substring(start, fullName.length)
- } else {
- fullName
- }
-
- test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
- assert(file.exists && file.isFile && file.canRead,
- "Benchmark %s is not a readable file".format(displayName))
-
- val ctx = createLeonContext((file.getPath +: leonOptions) :_*)
-
- val pipeline = mkPipeline
-
- if(forError) {
- intercept[LeonFatalError]{
- pipeline.run(ctx)(file.getPath :: Nil)
- }
- } else {
- val report = pipeline.run(ctx)(file.getPath :: Nil)
-
- block(Output(report, ctx.reporter))
- }
- }
- }
-
- private def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) {
- val fs = filesInResourceDir(
- "regression/verification/purescala/" + cat,
- _.endsWith(".scala"))
-
+// If you add another regression test, make sure it contains one object whose name matches the file name
+// This is because we compile all tests from each folder separately.
+class PureScalaVerificationRegression extends VerificationRegression {
+
+ val testDir = "regression/verification/purescala/"
+ val pipeFront = xlang.NoXLangFeaturesChecking
+ val pipeBack = AnalysisPhase
+ val optionVariants: List[List[String]] = {
val isZ3Available = try {
new Z3Interpreter()
true
@@ -73,24 +32,22 @@ class PureScalaVerificationRegression extends LeonTestSuite {
val isCVC4Available = try {
new CVC4Interpreter()
- // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
true
+ // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
} catch {
case e: java.io.IOException =>
false
}
- for(f <- fs) {
- mkTest(f, List("--feelinglucky"), forError)(block)
- mkTest(f, List("--codegen", "--evalground", "--feelinglucky"), forError)(block)
- mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky"), forError)(block)
- if (isZ3Available) {
- mkTest(f, List("--solvers=smt-z3", "--feelinglucky"), forError)(block)
- }
- if (isCVC4Available) {
- mkTest(f, List("--solvers=smt-cvc4", "--feelinglucky"), forError)(block)
- }
- }
+ List(
+ List("--feelinglucky"),
+ List("--codegen", "--evalground", "--feelinglucky"),
+ List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
+ ) ++ (
+ if (isZ3Available) List(List("--solvers=smt-z3", "--feelinglucky")) else Nil
+ ) ++ (
+ if (isCVC4Available) List(List("--solvers=smt-cvc4", "--feelinglucky")) else Nil
+ )
}
forEachFileIn("valid") { output =>
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d0b2e14aa3129cf65bc6c59fa6518df91e3ff938
--- /dev/null
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -0,0 +1,77 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.test.verification
+
+import leon._
+import leon.test._
+
+import leon.verification.VerificationReport
+import leon.purescala.Definitions.Program
+import leon.frontends.scalac.ExtractionPhase
+import leon.utils.PreprocessingPhase
+
+import _root_.smtlib.interpreters._
+
+import java.io.File
+
+// If you add another regression test, make sure it contains one object whose name matches the file name
+// This is because we compile all tests from each folder separately.
+trait VerificationRegression extends LeonTestSuite {
+
+ val optionVariants: List[List[String]]
+ val testDir: String
+
+ private var counter : Int = 0
+ private def nextInt() : Int = {
+ counter += 1
+ counter
+ }
+ private[verification] case class Output(report : VerificationReport, reporter : Reporter)
+
+ val pipeFront: Pipeline[Program, Program]
+ val pipeBack : Pipeline[Program, VerificationReport]
+
+ private def mkTest(files: List[String], leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
+ val extraction =
+ ExtractionPhase andThen
+ PreprocessingPhase andThen
+ pipeFront
+
+ if(forError) {
+ intercept[LeonFatalError]{
+ extraction.run(createLeonContext((files ++ leonOptions):_*))(files)
+ }
+ } else {
+ val ctx = createLeonContext(leonOptions:_*)
+ val ast = extraction.run(createLeonContext((files ++ leonOptions):_*))(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("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
+ val report = pipeBack.run(ctx)(p)
+ block(Output(report, ctx.reporter))
+ }
+ }
+ }
+
+ private[verification] def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) {
+ val fs = filesInResourceDir( testDir + cat, _.endsWith(".scala")).toList
+
+ fs foreach { file =>
+ assert(file.exists && file.isFile && file.canRead,
+ "Benchmark %s is not a readable file".format(file.getName))
+ }
+
+ val files = fs map { _.getPath }
+
+ // If error, try to verify each file separately (and fail for each one)
+ val groupedFiles = if (forError) files map (List(_)) else List(files)
+
+ for (files <- groupedFiles; options <- optionVariants) {
+ mkTest(files, options, forError)(block)
+ }
+ }
+
+
+}