diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala index 15b6bc3c434994b0b4fde1d1c420ee5d984c62fb..4c23831645433301166513a6f1792a678a6a00ed 100644 --- a/src/test/scala/leon/test/termination/TerminationRegression.scala +++ b/src/test/scala/leon/test/termination/TerminationRegression.scala @@ -54,17 +54,18 @@ class TerminationRegression extends LeonTestSuite { } } - private def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) { - val fs = filesInResourceDir( - "regression/termination/" + cat, - _.endsWith(".scala")) - - for(f <- fs) { + private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) { + for(f <- files) { mkTest(f, Seq(), forError)(block) } } - forEachFileIn("valid") { output => + def validFiles = filesInResourceDir("regression/termination/valid", _.endsWith(".scala")) ++ + filesInResourceDir("regression/verification/purescala/valid", _.endsWith(".scala")) + + def loopingFiles = filesInResourceDir("regression/termination/looping", _.endsWith(".scala")) + + forEachFileIn(validFiles) { output => val Output(report, reporter) = output val failures = report.results.collect { case (fd, guarantee) if !guarantee.isGuaranteed => fd } assert(failures.isEmpty, "Functions " + failures.map(_.id) + " should terminate") @@ -73,7 +74,7 @@ class TerminationRegression extends LeonTestSuite { assert(reporter.warningCount === 0) } - forEachFileIn("looping") { output => + forEachFileIn(loopingFiles) { output => val Output(report, reporter) = output val looping = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("looping") } assert(looping.forall(p => p._2.isInstanceOf[LoopsGivenInputs] || p._2.isInstanceOf[CallsNonTerminating]),