diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala index 26513352be7221aa54864e15112c8a7936c78090..834597e79adce7675e1190359aee34e864ccf37f 100644 --- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala @@ -2,106 +2,13 @@ package leon.regression.verification -import leon._ -import leon.test._ - -import leon.verification.{AnalysisPhase, VerificationReport} -import leon.xlang.FixReportLabels -import leon.frontends.scalac.ExtractionPhase -import leon.utils.PreprocessingPhase - -import _root_.smtlib.interpreters._ - -import java.io.File - -class XLangVerificationSuite extends LeonRegressionSuite { - private var counter : Int = 0 - private def nextInt() : Int = { - counter += 1 - counter - } - private case class Output(report : VerificationReport, reporter : Reporter) - - private def mkPipeline : Pipeline[List[String],VerificationReport] = - ExtractionPhase andThen - new PreprocessingPhase(desugarXLang = true) andThen - AnalysisPhase andThen - FixReportLabels - - private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = { - val fullName = file.getPath - val start = fullName.indexOf("regression") - - val displayName = if(start != -1) { - fullName.substring(start, fullName.length) - } else { - fullName - } - - val ignored = List() - - val t = if (ignored.exists(displayName endsWith _)) { - ignore _ - } else { - test _ - } - - t(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}", Nil) { - assert(file.exists && file.isFile && file.canRead, - s"Benchmark $displayName is not a readable file") - - val ctx = createLeonContext((file.getPath +: leonOptions) :_*) - - val pipeline = mkPipeline - - if(forError) { - intercept[LeonFatalError]{ - pipeline.run(ctx, file.getPath :: Nil) - } - } else { - val (ctx2, report) = pipeline.run(ctx, file.getPath :: Nil) - - block(Output(report, ctx2.reporter)) - } - } - } - - - private def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) { - val fs = filesInResourceDir( - "regression/verification/xlang/" + cat, - _.endsWith(".scala")) - - val isZ3Available = try { - Z3Interpreter.buildDefault.free() - true - } catch { - case e: java.io.IOException => - false - } - - for(f <- fs) { - mkTest(f, List(), forError)(block) - mkTest(f, List("--feelinglucky"), forError)(block) - if (isZ3Available) { - mkTest(f, List("--solvers=smt-z3", "--feelinglucky"), forError)(block) - } - } - } - - forEachFileIn("valid") { output => - val Output(report, reporter) = output - assert(report.totalConditions === report.totalValid, - "All verification conditions ("+report.totalConditions+") should be valid.") - assert(reporter.errorCount === 0) - } - - forEachFileIn("invalid") { output => - val Output(report, _) = output - assert(report.totalInvalid > 0, - "There should be at least one invalid verification condition.") - assert(report.totalUnknown === 0, - "There should not be unknown verification conditions.") - } - +class XLangVerificationSuite extends VerificationSuite { + + val optionVariants: List[List[String]] = List( + List(), + List("--feelinglucky"), + List("--solvers=smt-z3", "--feelinglucky") + ) + val testDir: String = "regression/verification/xlang/" + override val desugarXLang = true }