diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala index 58bd519b728a8867abb7bf03350b054b8d673b2c..0da9e68bba08fb1d8ca7b4a41195384e0118fd26 100644 --- a/src/test/scala/leon/test/LeonTestSuite.scala +++ b/src/test/scala/leon/test/LeonTestSuite.scala @@ -13,7 +13,7 @@ import org.scalatest.exceptions.TestFailedException import java.io.File -trait LeonTestSuite extends FunSuite with Timeouts { +trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach { def now() = { System.currentTimeMillis } @@ -42,10 +42,11 @@ trait LeonTestSuite extends FunSuite with Timeouts { Main.processOptions(opts.toList).copy(reporter = reporter, interruptManager = new InterruptManager(reporter)) } - var testContext = generateContext + var testContext: LeonContext = null - def generateContext = { - createLeonContext() + override def beforeEach() = { + testContext = createLeonContext() + super.beforeEach() } def testIdentifier(name: String): String = { @@ -104,8 +105,6 @@ trait LeonTestSuite extends FunSuite with Timeouts { val ts = now() - testContext = generateContext - failAfter(5.minutes) { try { body diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala index d3123f4d209086b20a04b33594d5c1c4070a9ef0..2a126a2443763ab18f1c2efd5b8068d126a87ce3 100644 --- a/src/test/scala/leon/test/purescala/TransformationTests.scala +++ b/src/test/scala/leon/test/purescala/TransformationTests.scala @@ -19,12 +19,6 @@ class TransformationTests extends LeonTestSuite { val pipeline = ExtractionPhase andThen PreprocessingPhase filesInResourceDir("regression/transformations").foreach { file => - val ctx = testContext.copy( - files = List(file) - ) - - val prog = pipeline.run(ctx)(file.getPath :: Nil) - // Configure which file corresponds to which transformation: val (title: String, transformer: (Expr => Expr)) = file.getName match { @@ -42,20 +36,27 @@ class TransformationTests extends LeonTestSuite { fail("Unknown name "+n) } + test(title) { + val ctx = testContext.copy( + files = List(file) + ) + + val prog = pipeline.run(ctx)(file.getPath :: Nil) + - // Proceed with the actual tests - val inputs = prog.definedFunctions.collect{ - case fd if fd.id.name.startsWith("input") => - (fd.id.name.substring(5,7), fd) - }.toSeq.sortBy(_._1) + // Proceed with the actual tests + val inputs = prog.definedFunctions.collect{ + case fd if fd.id.name.startsWith("input") => + (fd.id.name.substring(5,7), fd) + }.toSeq.sortBy(_._1) - val outputs = prog.definedFunctions.collect{ - case fd if fd.id.name.startsWith("output") => - (fd.id.name.substring(6,8), fd) - }.toMap + val outputs = prog.definedFunctions.collect{ + case fd if fd.id.name.startsWith("output") => + (fd.id.name.substring(6,8), fd) + }.toMap - for ((n, fdin) <- inputs) { - test(title +" ["+n+"]") { + for ((n, fdin) <- inputs) { + info(title +" ["+n+"]") val in = fdin.body.get outputs.get(n) match { case Some(fdexp) => diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala index 32eee19c2443aebd041e7db450a6e849e9c67f51..a6794621b422602d2e7c03326f5ed3d6a4aa4a5e 100644 --- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala +++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala @@ -26,15 +26,19 @@ class SynthesisRegressionSuite extends LeonTestSuite { private def testSynthesis(cat: String, f: File, bound: Int) { - val ctx = createLeonContext("--synthesis", "--library") + var chooses = List[ChooseInfo]() - val opts = SynthesisOptions(searchBound = Some(bound), allSeeing = true) + test(cat+": "+f.getName()+" Compilation") { + val ctx = createLeonContext("--synthesis", "--library") - val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase + val opts = SynthesisOptions(searchBound = Some(bound), allSeeing = true) - val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil) + val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase - var chooses = ChooseInfo.extractFromProgram(ctx, program, opts) + val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil) + + chooses = ChooseInfo.extractFromProgram(ctx, program, opts) + } for (ci <- chooses) { test(cat+": "+f.getName()+" - "+ci.fd.id.name) { diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala index ab07f81169b75c96cfbe836f5d2aee282539e7bb..ea7a93310f7757c5d0b672e326980a8f0a9874e6 100644 --- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala +++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala @@ -26,19 +26,20 @@ class SynthesisSuite extends LeonTestSuite { def forProgram(title: String, opts: SynthesisOptions = SynthesisOptions())(content: String)(block: (SynthesisContext, FunDef, Problem) => Unit) { - val ctx = testContext.copy(settings = Settings( - synthesis = true, - xlang = false, - verify = false - )) + test("Synthesizing %3d: [%s]".format(nextInt(), title)) { + val ctx = testContext.copy(settings = Settings( + synthesis = true, + xlang = false, + verify = false + )) + + val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen PreprocessingPhase andThen SynthesisProblemExtractionPhase - try { - val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen PreprocessingPhase andThen SynthesisProblemExtractionPhase + val (program, results) = pipeline.run(ctx)((content, Nil)) - val (program, results) = pipeline.run(ctx)((content, Nil)) + for ((f, ps) <- results; p <- ps) { + info("%-20s".format(f.id.toString)) - for ((f, ps) <- results; p <- ps) { - test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) { val sctx = SynthesisContext(ctx, opts, Some(f), @@ -48,12 +49,6 @@ class SynthesisSuite extends LeonTestSuite { block(sctx, f, p) } } - } catch { - case lfe: LeonFatalError => - test("Synthesizing %3d: %-20s [%s]".format(nextInt(), "", title)) { - assert(false, "Failed to compile "+title) - } - } } case class Apply(desc: String, andThen: List[Apply] = Nil)