From 18d982896409cd5016dcfed0183f1c475a311558 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Tue, 2 Jun 2015 21:41:18 +0200
Subject: [PATCH] run TerminationRegression test also on all tests for
verification
---
.../termination/TerminationRegression.scala | 17 +++++++++--------
1 file changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 15b6bc3c4..4c2383164 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]),
--
GitLab