Skip to content
Snippets Groups Projects
Commit 20291961 authored by Etienne Kneuss's avatar Etienne Kneuss Committed by Manos Koukoutos
Browse files

Fix VerificationSuite

Fix how names are printed
Fix how tests are ignored
Ignore correct tests
parent dee93143
Branches
Tags
No related merge requests found
...@@ -34,6 +34,7 @@ class TerminationSuite extends LeonRegressionSuite { ...@@ -34,6 +34,7 @@ class TerminationSuite extends LeonRegressionSuite {
val ignored = List( val ignored = List(
"verification/purescala/valid/MergeSort.scala", "verification/purescala/valid/MergeSort.scala",
"verification/purescala/valid/Nested14.scala",
"verification/purescala/valid/InductiveQuantification.scala" "verification/purescala/valid/InductiveQuantification.scala"
) )
......
...@@ -15,6 +15,12 @@ class PureScalaVerificationSuite extends VerificationSuite { ...@@ -15,6 +15,12 @@ class PureScalaVerificationSuite extends VerificationSuite {
val testDir = "regression/verification/purescala/" val testDir = "regression/verification/purescala/"
val pipeFront = xlang.NoXLangFeaturesChecking val pipeFront = xlang.NoXLangFeaturesChecking
val pipeBack = AnalysisPhase val pipeBack = AnalysisPhase
override val ignored = Seq(
"verification/purescala/valid/Nested15.scala",
"verification/purescala/invalid/Nested15.scala"
)
val optionVariants: List[List[String]] = { val optionVariants: List[List[String]] = {
val isZ3Available = try { val isZ3Available = try {
Z3Interpreter.buildDefault.free() Z3Interpreter.buildDefault.free()
......
...@@ -19,6 +19,8 @@ trait VerificationSuite extends LeonRegressionSuite { ...@@ -19,6 +19,8 @@ trait VerificationSuite extends LeonRegressionSuite {
val optionVariants: List[List[String]] val optionVariants: List[List[String]]
val testDir: String val testDir: String
val ignored: Seq[String] = Seq()
private var counter: Int = 0 private var counter: Int = 0
private def nextInt(): Int = { private def nextInt(): Int = {
counter += 1 counter += 1
...@@ -42,11 +44,19 @@ trait VerificationSuite extends LeonRegressionSuite { ...@@ -42,11 +44,19 @@ trait VerificationSuite extends LeonRegressionSuite {
val (ctx2, ast) = extraction.run(ctx, files) val (ctx2, ast) = extraction.run(ctx, files)
val programs = { val programs = {
val (user, lib) = ast.units partition { _.isMainUnit } val (user, lib) = ast.units partition { _.isMainUnit }
user map { u => (u.id, Program(u :: lib)) } user map ( u => Program(u :: lib) )
} }
for ((id, p) <- programs; options <- optionVariants) { for ( p <- programs; options <- optionVariants) {
val displayName = s"$cat/${p.units.head.id.name}.scala"
val index = nextInt() val index = nextInt()
test(f"$index%3d: ${id.name} ${options.mkString(" ")}") { val ts = if (ignored exists (_.endsWith(displayName)))
ignore _
else
test _
ts(f"$index%3d: $displayName ${options.mkString(" ")}", Seq()) {
val ctx = createLeonContext(options: _*) val ctx = createLeonContext(options: _*)
if (forError) { if (forError) {
intercept[LeonFatalError] { intercept[LeonFatalError] {
......
...@@ -38,9 +38,7 @@ class XLangVerificationSuite extends LeonRegressionSuite { ...@@ -38,9 +38,7 @@ class XLangVerificationSuite extends LeonRegressionSuite {
fullName fullName
} }
val ignored = List( val ignored = List()
"regression/verification/xlang/valid/Nested15.scala"
)
val t = if (ignored.exists(displayName endsWith _)) { val t = if (ignored.exists(displayName endsWith _)) {
ignore _ ignore _
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment