diff --git a/src/test/resources/regression/verification/purescala/error/Asserts.scala b/src/test/resources/regression/frontends/error/simple/Asserts.scala
similarity index 100%
rename from src/test/resources/regression/verification/purescala/error/Asserts.scala
rename to src/test/resources/regression/frontends/error/simple/Asserts.scala
diff --git a/src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala b/src/test/resources/regression/frontends/error/simple/ConvertBigInt.scala
similarity index 100%
rename from src/test/resources/regression/verification/purescala/error/ConvertBigInt.scala
rename to src/test/resources/regression/frontends/error/simple/ConvertBigInt.scala
diff --git a/src/test/resources/regression/verification/purescala/error/InstanceOf1.scala b/src/test/resources/regression/frontends/error/simple/InstanceOf1.scala
similarity index 100%
rename from src/test/resources/regression/verification/purescala/error/InstanceOf1.scala
rename to src/test/resources/regression/frontends/error/simple/InstanceOf1.scala
diff --git a/src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala b/src/test/resources/regression/frontends/error/simple/LiteralBigInt.scala
similarity index 100%
rename from src/test/resources/regression/verification/purescala/error/LiteralBigInt.scala
rename to src/test/resources/regression/frontends/error/simple/LiteralBigInt.scala
diff --git a/src/test/resources/regression/verification/purescala/error/NotEquals.scala b/src/test/resources/regression/frontends/error/simple/NotEquals.scala
similarity index 100%
rename from src/test/resources/regression/verification/purescala/error/NotEquals.scala
rename to src/test/resources/regression/frontends/error/simple/NotEquals.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array1.scala b/src/test/resources/regression/frontends/error/xlang/Array1.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array1.scala
rename to src/test/resources/regression/frontends/error/xlang/Array1.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array10.scala b/src/test/resources/regression/frontends/error/xlang/Array10.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array10.scala
rename to src/test/resources/regression/frontends/error/xlang/Array10.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array2.scala b/src/test/resources/regression/frontends/error/xlang/Array2.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array2.scala
rename to src/test/resources/regression/frontends/error/xlang/Array2.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array3.scala b/src/test/resources/regression/frontends/error/xlang/Array3.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array3.scala
rename to src/test/resources/regression/frontends/error/xlang/Array3.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array4.scala b/src/test/resources/regression/frontends/error/xlang/Array4.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array4.scala
rename to src/test/resources/regression/frontends/error/xlang/Array4.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array5.scala b/src/test/resources/regression/frontends/error/xlang/Array5.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array5.scala
rename to src/test/resources/regression/frontends/error/xlang/Array5.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array6.scala b/src/test/resources/regression/frontends/error/xlang/Array6.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array6.scala
rename to src/test/resources/regression/frontends/error/xlang/Array6.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array7.scala b/src/test/resources/regression/frontends/error/xlang/Array7.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array7.scala
rename to src/test/resources/regression/frontends/error/xlang/Array7.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array8.scala b/src/test/resources/regression/frontends/error/xlang/Array8.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array8.scala
rename to src/test/resources/regression/frontends/error/xlang/Array8.scala
diff --git a/src/test/resources/regression/verification/xlang/error/Array9.scala b/src/test/resources/regression/frontends/error/xlang/Array9.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/error/Array9.scala
rename to src/test/resources/regression/frontends/error/xlang/Array9.scala
diff --git a/src/test/resources/regression/frontends/Fields.scala b/src/test/resources/regression/frontends/passing/Fields.scala
similarity index 100%
rename from src/test/resources/regression/frontends/Fields.scala
rename to src/test/resources/regression/frontends/passing/Fields.scala
diff --git a/src/test/resources/regression/frontends/Operators.scala b/src/test/resources/regression/frontends/passing/Operators.scala
similarity index 100%
rename from src/test/resources/regression/frontends/Operators.scala
rename to src/test/resources/regression/frontends/passing/Operators.scala
diff --git a/src/test/scala/leon/test/frontends/FrontEndsTest.scala b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
index c5b7e63fb2311544fa945787b66576ab1c41013b..90335806c2eb597b31becd36e78d609267a49373 100644
--- a/src/test/scala/leon/test/frontends/FrontEndsTest.scala
+++ b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
@@ -3,11 +3,29 @@
package leon.test.frontends
import leon._
+import test.LeonTestSuite
+import purescala.Definitions.Program
import java.io.File
-class FrontEndsTest extends leon.test.LeonTestSuite {
+class FrontEndsTest extends LeonTestSuite {
// Hard-code output directory, for Eclipse purposes
- lazy val tmpPath = java.nio.file.Files.createTempDirectory("leon-frontends");
+
+ val pipeFront = frontends.scalac.ExtractionPhase andThen utils.PreprocessingPhase
+
+ def testFrontend(f: File, pipeBack: Pipeline[Program, Program], forError: Boolean) = {
+ val pipeline = pipeFront andThen pipeBack
+ test ("Testing " + f.getName) {
+ val ctx = createLeonContext()
+ if (forError) {
+ intercept[LeonFatalError]{
+ pipeline.run(ctx)(List(f.getAbsolutePath()))
+ }
+ } else {
+ pipeline.run(ctx)(List(f.getAbsolutePath()))
+ }
+ }
+
+ }
private def forEachFileIn(path : String)(block : File => Unit) {
val fs = filesInResourceDir(path, _.endsWith(".scala"))
@@ -16,54 +34,19 @@ class FrontEndsTest extends leon.test.LeonTestSuite {
block(f)
}
}
-
- val pipeline1 =
- frontends.scalac.ExtractionPhase andThen
- utils.ScopingPhase andThen
- purescala.MethodLifting andThen
- utils.TypingPhase andThen
- purescala.CompleteAbstractDefinitions andThen
- utils.FileOutputPhase
-
- val pipeline2 =
- frontends.scalac.ExtractionPhase andThen
- utils.ScopingPhase andThen
- purescala.MethodLifting andThen
- utils.TypingPhase andThen
- purescala.CompleteAbstractDefinitions andThen
- purescala.RestoreMethods andThen
- utils.FileOutputPhase
-
- forEachFileIn("regression/frontends" ) { f =>
- testExtr(f)
- }
-
- def testExtr(f : File) {
- val outFileName1 = tmpPath.toString ++ "/" ++ f.getName
- val outFileName2 = tmpPath.toString ++ "/restored" ++ f.getName
- test ("Testing " + f.getName) {
- // Compile original file
- val timeOut = 2
- val settings = testContext.settings.copy(
- debugSections = Set()
- )
- val ctx1 = testContext.copy(
- // We want a reporter that actually prints some output
- //reporter = new DefaultReporter(settings),
- settings = settings,
- options = testContext.options :+ LeonValueOption("o", outFileName1)
- )
-
- val ctx2 = ctx1.copy(
- //reporter = new DefaultReporter(settings),
- settings = settings,
- options = testContext.options :+ LeonValueOption("o", outFileName2 )
- )
-
- pipeline1.run(ctx1)(List(f.getAbsolutePath()))
- pipeline2.run(ctx2)(List(f.getAbsolutePath()))
- }
-
+ val pipeNormal = xlang.NoXLangFeaturesChecking andThen NoopPhase() // redundant NoopPhase to trigger throwing error between phases
+ val pipeX = NoopPhase[Program]()
+ val baseDir = "regression/frontends/"
+
+ forEachFileIn(baseDir+"passing/") { f =>
+ testFrontend(f, pipeNormal, false)
+ }
+ forEachFileIn(baseDir+"error/simple/") { f =>
+ testFrontend(f, pipeNormal, true)
}
+ forEachFileIn(baseDir+"error/xlang/") { f =>
+ testFrontend(f, pipeX, true)
+ }
+
}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index c907a66569bee4906fce477d9216afd8a278cd75..51aa4fced083cb589898609bc089c8a684bd941c 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -67,6 +67,5 @@ class PureScalaVerificationRegression extends VerificationRegression {
assert(reporter.errorCount >= report.totalInvalid)
assert(reporter.warningCount === 0)
}
- forEachFileIn("error", true) { output => () }
}
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index d0b2e14aa3129cf65bc6c59fa6518df91e3ff938..210a5ab7e5e3a67e02fbc4c63ce6b61f63162b60 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -31,27 +31,21 @@ trait VerificationRegression extends LeonTestSuite {
val pipeFront: Pipeline[Program, Program]
val pipeBack : Pipeline[Program, VerificationReport]
- private def mkTest(files: List[String], leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
+ private def mkTest(files: List[String], leonOptions : Seq[String])(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))
- }
+ 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))
}
}
@@ -65,11 +59,8 @@ trait VerificationRegression extends LeonTestSuite {
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)
+ for (options <- optionVariants) {
+ mkTest(files, options)(block)
}
}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index f331b1c119100f2c723a50a7a81fb684ef225828..83e89516991052b4d83103461941631fe6d74065 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -106,6 +106,4 @@ class XLangVerificationRegression extends LeonTestSuite {
assert(reporter.errorCount >= report.totalInvalid)
}
- forEachFileIn("error", true) { output => () }
-
}