diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index a0d5c4830ffd69b47478593e823217960b2aa21d..6dbc05306c67196944a0d5a5b52cce1b011ace82 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -15,8 +15,9 @@ object Main {
xlang.ArrayTransformation,
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
- purescala.FunctionClosure,
+ xlang.FixReportLabels,
xlang.XLangAnalysisPhase,
+ purescala.FunctionClosure,
synthesis.SynthesisPhase,
termination.TerminationPhase,
verification.AnalysisPhase,
@@ -39,16 +40,15 @@ object Main {
val description = "Options that select the feature of Leon to be used. Default: verify"
val optEval = LeonStringOptionDef("eval", "Evaluate ground functions through code generation or evaluation (default)", "default", "[code|default]")
- val optXLang = LeonFlagOptionDef("xlang", "Verification with support for extra program constructs (imperative,...)", false)
- val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
- val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
- val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
- val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
- val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
- val optHelp = LeonFlagOptionDef("help", "Show help message", false)
+ val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
+ val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
+ val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
+ val optHelp = LeonFlagOptionDef("help", "Show help message", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optEval, optVerify)
+ Set(optTermination, optRepair, optSynthesis, optNoop, optHelp, optEval, optVerify)
}
@@ -140,7 +140,7 @@ object Main {
import frontends.scalac.ExtractionPhase
import synthesis.SynthesisPhase
import termination.TerminationPhase
- import xlang.XLangAnalysisPhase
+ import xlang.{XLangAnalysisPhase, FixReportLabels}
import verification.AnalysisPhase
import repair.RepairPhase
import evaluators.EvaluationPhase
@@ -149,7 +149,7 @@ object Main {
val helpF = ctx.findOptionOrDefault(optHelp)
val noopF = ctx.findOptionOrDefault(optNoop)
val synthesisF = ctx.findOptionOrDefault(optSynthesis)
- val xlangF = ctx.findOptionOrDefault(optXLang)
+ val xlangF = ctx.findOptionOrDefault(SharedOptions.optXLang)
val repairF = ctx.findOptionOrDefault(optRepair)
val terminationF = ctx.findOptionOrDefault(optTermination)
val verifyF = ctx.findOptionOrDefault(optVerify)
@@ -173,7 +173,9 @@ object Main {
ExtractionPhase andThen
debugTrees("Program after extraction") andThen
PreprocessingPhase andThen
- debugTrees("Program after pre-processing")
+ debugTrees("Program after pre-processing") andThen
+ XLangAnalysisPhase andThen
+ debugTrees("Program after xlang desugaring")
else
ExtractionPhase andThen
debugTrees("Program after extraction") andThen
@@ -181,15 +183,19 @@ object Main {
debugTrees("Program after pre-processing") andThen
xlang.NoXLangFeaturesChecking
+ val analysis = if (xlangF) AnalysisPhase andThen FixReportLabels else AnalysisPhase
+
val pipeProcess: Pipeline[Program, Any] = {
if (noopF) RestoreMethods andThen FileOutputPhase
else if (synthesisF) SynthesisPhase
else if (repairF) RepairPhase
- else if (analysisF) Pipeline.both(FunctionClosure andThen AnalysisPhase, TerminationPhase)
+ else if (analysisF) Pipeline.both(
+ FunctionClosure andThen analysis,
+ TerminationPhase
+ )
else if (terminationF) TerminationPhase
- else if (xlangF) XLangAnalysisPhase
else if (evalF) EvaluationPhase
- else FunctionClosure andThen AnalysisPhase
+ else FunctionClosure andThen analysis
}
pipeBegin andThen
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 369043e66c5eb41151ed20248ae1aee15322d5ba..3884b00c0fe0b7eefb99d68a04aa0d528afe9672 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -18,6 +18,8 @@ object SharedOptions extends LeonComponent {
val optStrictPhases = LeonFlagOptionDef("strict", "Terminate after each phase if there is an error", true)
+ val optXLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false)
+
val optWatch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false)
val optFunctions = new LeonOptionDef[Seq[String]] {
@@ -69,6 +71,7 @@ object SharedOptions extends LeonComponent {
override val definedOptions: Set[LeonOptionDef[Any]] = Set(
optStrictPhases,
+ optXLang,
optFunctions,
optSelectedSolvers,
optDebug,
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index d95d4530eed390f8e74dec670fd572bd70fe7034..811b4a2b980de6ffcc2d5484ebfaf8a9c31972fd 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -541,23 +541,20 @@ trait CodeExtraction extends ASTExtractors {
classesToClasses += sym -> ccd
// Validates type parameters
- parent match {
- case Some(pct) =>
- if(pct.classDef.tparams.size == tparams.size) {
- val pcd = pct.classDef
- val ptps = pcd.tparams.map(_.tp)
+ parent foreach { pct =>
+ if(pct.classDef.tparams.size == tparams.size) {
+ val pcd = pct.classDef
+ val ptps = pcd.tparams.map(_.tp)
- val targetType = AbstractClassType(pcd, ptps)
- val fromChild = CaseClassType(ccd, ptps).parent.get
+ val targetType = AbstractClassType(pcd, ptps)
+ val fromChild = CaseClassType(ccd, ptps).parent.get
- if (fromChild != targetType) {
- outOfSubsetError(sym.pos, "Child type should form a simple bijection with parent class type (e.g. C[T1,T2] extends P[T1,T2])")
- }
-
- } else {
- outOfSubsetError(sym.pos, "Child classes should have the same number of type parameters as their parent")
+ if (fromChild != targetType) {
+ outOfSubsetError(sym.pos, "Child type should form a simple bijection with parent class type (e.g. C[T1,T2] extends P[T1,T2])")
}
- case _ =>
+ } else {
+ outOfSubsetError(sym.pos, "Child classes should have the same number of type parameters as their parent")
+ }
}
ccd
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index b91ca4e3f34e2b9ca81decc6fb36d928e1315973..bedc124db6558eac471283c1750f16babacf9430 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -58,12 +58,11 @@ object FunctionClosure extends TransformationPhase {
val extraValDefs: Seq[ValDef] = extraValDefFreshIds.map(ValDef(_))
val newValDefs: Seq[ValDef] = fd.params ++ extraValDefs
val newBindedVars: Set[Identifier] = bindedVars ++ fd.params.map(_.id)
- val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
+ val newFunId = FreshIdentifier(fd.id.name, alwaysShowUniqueID = true) //since we hoist this at the top level, we need to make it a unique name
val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs).copiedFrom(fd)
topLevelFuns += newFunDef
newFunDef.copyContentFrom(fd) //TODO: this still has some dangerous side effects (?)
- newFunDef.addFlag(IsLoop(fd))
def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 0667ed67271b076df8ee7de496c9a1a038281798..dd15dda2a3d619558c04e57ec40818e467fea529 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -9,7 +9,6 @@ import VCStatus._
import purescala.Definitions.FunDef
case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
- import scala.math.Ordering.Implicits._
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
diff --git a/src/main/scala/leon/xlang/ExprOps.scala b/src/main/scala/leon/xlang/ExprOps.scala
index 4e38794c9894da96057815aace86cc1c8411e08f..0f2a4db3d926d889df6fd5d7fa0f2548c6578209 100644
--- a/src/main/scala/leon/xlang/ExprOps.scala
+++ b/src/main/scala/leon/xlang/ExprOps.scala
@@ -10,17 +10,11 @@ import purescala.ExprOps._
object ExprOps {
def isXLang(expr: Expr): Boolean = exists {
- case Block(_, _) | Assignment(_, _) |
- While(_, _) | Epsilon(_, _) |
- EpsilonVariable(_, _) |
- LetVar(_, _, _) | Waypoint(_, _, _) |
- ArrayUpdate(_, _, _)
- => true
- case _ => false
+ _.isInstanceOf[XLangExpr]
}(expr)
def containsEpsilon(e: Expr) = exists{
- case (l: Epsilon) => true
+ case _ : Epsilon => true
case _ => false
}(e)
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index 9d566e46dab859f0520fdeba161bf890848b790d..237636db74d6b92d74704114713e7270836f4e2d 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -13,7 +13,9 @@ import utils._
object Expressions {
import purescala.PrinterHelpers._
- case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable {
+ trait XLangExpr extends Expr
+
+ case class Block(exprs: Seq[Expr], last: Expr) extends XLangExpr with NAryExtractable with PrettyPrintable {
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
}
@@ -31,7 +33,7 @@ object Expressions {
val getType = last.getType
}
- case class Assignment(varId: Identifier, expr: Expr) extends Expr with UnaryExtractable with PrettyPrintable {
+ case class Assignment(varId: Identifier, expr: Expr) extends XLangExpr with UnaryExtractable with PrettyPrintable {
val getType = UnitType
def extract: Option[(Expr, (Expr)=>Expr)] = {
@@ -43,7 +45,7 @@ object Expressions {
}
}
- case class While(cond: Expr, body: Expr) extends Expr with NAryExtractable with PrettyPrintable {
+ case class While(cond: Expr, body: Expr) extends XLangExpr with NAryExtractable with PrettyPrintable {
val getType = UnitType
var invariant: Option[Expr] = None
@@ -72,7 +74,7 @@ object Expressions {
}
}
- case class Epsilon(pred: Expr, tpe: TypeTree) extends Expr with UnaryExtractable with PrettyPrintable {
+ case class Epsilon(pred: Expr, tpe: TypeTree) extends XLangExpr with UnaryExtractable with PrettyPrintable {
def extract: Option[(Expr, (Expr)=>Expr)] = {
Some((pred, (expr: Expr) => Epsilon(expr, this.getType).setPos(this)))
}
@@ -84,7 +86,7 @@ object Expressions {
val getType = tpe
}
- case class EpsilonVariable(pos: Position, tpe: TypeTree) extends Expr with Terminal with PrettyPrintable {
+ case class EpsilonVariable(pos: Position, tpe: TypeTree) extends XLangExpr with Terminal with PrettyPrintable {
def printWith(implicit pctx: PrinterContext) {
p"x${pos.line}_${pos.col}"
@@ -94,7 +96,7 @@ object Expressions {
}
//same as let, buf for mutable variable declaration
- case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable with PrettyPrintable {
+ case class LetVar(binder: Identifier, value: Expr, body: Expr) extends XLangExpr with BinaryExtractable with PrettyPrintable {
val getType = body.getType
def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)] = {
@@ -109,7 +111,7 @@ object Expressions {
}
}
- case class Waypoint(i: Int, expr: Expr, tpe: TypeTree) extends Expr with UnaryExtractable with PrettyPrintable{
+ case class Waypoint(i: Int, expr: Expr, tpe: TypeTree) extends XLangExpr with UnaryExtractable with PrettyPrintable{
def extract: Option[(Expr, (Expr)=>Expr)] = {
Some((expr, (e: Expr) => Waypoint(i, e, tpe)))
}
@@ -121,7 +123,7 @@ object Expressions {
val getType = tpe
}
- case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with NAryExtractable with PrettyPrintable {
+ case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends XLangExpr with NAryExtractable with PrettyPrintable {
val getType = UnitType
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
new file mode 100644
index 0000000000000000000000000000000000000000..37c3fef240ddbaf49bc336421257fd354cadf1ec
--- /dev/null
+++ b/src/main/scala/leon/xlang/FixReportLabels.scala
@@ -0,0 +1,46 @@
+
+package leon
+package xlang
+
+import leon.purescala.Definitions.IsLoop
+import leon.verification.{VC, VCKinds, VerificationReport}
+import leon.xlang.XLangAnalysisPhase.VCXLangKinds._
+
+object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]{
+
+ override val name: String = "fixReportLabels"
+ override val description: String = "Fix verification report labels to reflect the original imperative VCs"
+
+ def run(ctx: LeonContext)(vr: VerificationReport): VerificationReport = {
+ //this is enough to convert invariant postcondition and inductive conditions. However the initial validity
+ //of the invariant (before entering the loop) will still appear as a regular function precondition
+ //To fix this, we need some information in the VCs about which function the precondtion refers to
+ //although we could arguably say that the term precondition is general enough to refer both to a loop invariant
+ //precondition and a function invocation precondition
+
+ val newResults = for ((vc, ovr) <- vr.results) yield {
+ val (vcKind, fd) = vc.fd.flags.collectFirst { case IsLoop(orig) => orig } match {
+ case None => (vc.kind, vc.fd)
+ case Some(owner) => (vc.kind.underlying match {
+ case VCKinds.Precondition => InvariantInd
+ case VCKinds.Postcondition => InvariantPost
+ case _ => vc.kind
+ }, owner)
+ }
+
+ val nvc = VC(
+ vc.condition,
+ fd,
+ vcKind,
+ vc.tactic
+ ).setPos(vc.getPos)
+
+ nvc -> ovr
+
+ }
+
+ VerificationReport(newResults)
+
+ }
+
+}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 9678009e6b16ead52fa489c386afa5b60a75c810..ec24b4c93f642e02390c5add25fde7a13910684f 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -17,42 +17,38 @@ object ImperativeCodeElimination extends TransformationPhase {
val name = "Imperative Code Elimination"
val description = "Transform imperative constructs into purely functional code"
- private var varInScope = Set[Identifier]()
- private var parent: FunDef = null //the enclosing fundef
-
def apply(ctx: LeonContext, pgm: Program): Program = {
- varInScope = Set()
- parent = null
-
val allFuns = pgm.definedFunctions
for {
fd <- allFuns
body <- fd.body
} {
- parent = fd
- val (res, scope, _) = toFunction(body)
+ val (res, scope, _) = toFunction(body)(State(fd, Set()))
fd.body = Some(scope(res))
}
pgm
}
+ case class State(parent: FunDef, varsInScope: Set[Identifier]) {
+ def withVar(i: Identifier) = copy(varsInScope = varsInScope + i)
+ }
+
//return a "scope" consisting of purely functional code that defines potentially needed
//new variables (val, not var) and a mapping for each modified variable (var, not val :) )
//to their new name defined in the scope. The first returned valued is the value of the expression
//that should be introduced as such in the returned scope (the val already refers to the new names)
- private def toFunction(expr: Expr): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
+ private def toFunction(expr: Expr)(implicit state: State): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
+ import state._
val res = expr match {
case LetVar(id, e, b) => {
val newId = id.freshen
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
- varInScope += id
- val (bodyRes, bodyScope, bodyFun) = toFunction(b)
- varInScope -= id
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withVar(id))
val scope = (body: Expr) => rhsScope(Let(newId, rhsVal, replaceNames(rhsFun + (id -> newId), bodyScope(body))).copiedFrom(expr))
(bodyRes, scope, (rhsFun + (id -> newId)) ++ bodyFun)
}
case Assignment(id, e) => {
- assert(varInScope.contains(id))
+ assert(varsInScope.contains(id))
val newId = id.freshen
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
val scope = (body: Expr) => rhsScope(Let(newId, rhsVal, body).copiedFrom(expr))
@@ -66,7 +62,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val iteRType = leastUpperBound(tRes.getType, eRes.getType).get
- val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varInScope).toSeq
+ val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varsInScope).toSeq
val resId = FreshIdentifier("res", iteRType)
val freshIds = modifiedVars.map( { _.freshen })
val iteType = tupleTypeWrap(resId.getType +: freshIds.map(_.getType))
@@ -102,7 +98,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val (csesRes, csesScope, csesFun) = csesRhs.map(toFunction).unzip3
val (scrutRes, scrutScope, scrutFun) = toFunction(scrut)
- val modifiedVars: Seq[Identifier] = csesFun.toSet.flatMap((m: Map[Identifier, Identifier]) => m.keys).intersect(varInScope).toSeq
+ val modifiedVars: Seq[Identifier] = csesFun.toSet.flatMap((m: Map[Identifier, Identifier]) => m.keys).intersect(varsInScope).toSeq
val resId = FreshIdentifier("res", m.getType)
val freshIds = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
val matchType = tupleTypeWrap(resId.getType +: freshIds.map(_.getType))
@@ -141,7 +137,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val (_, bodyScope, bodyFun) = toFunction(body)
val condBodyFun = condFun ++ bodyFun
- val modifiedVars: Seq[Identifier] = condBodyFun.keys.toSet.intersect(varInScope).toSeq
+ val modifiedVars: Seq[Identifier] = condBodyFun.keys.toSet.intersect(varsInScope).toSeq
if(modifiedVars.isEmpty)
(UnitLiteral(), (b: Expr) => b, Map())
@@ -150,7 +146,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunValDefs = whileFunVars.map(ValDef(_))
val whileFunReturnType = tupleTypeWrap(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs).setPos(wh)
+ val whileFunDef = new FunDef(parent.id.freshen, Nil, whileFunReturnType, whileFunValDefs).setPos(wh)
whileFunDef.addFlag(IsLoop(parent))
val whileFunCond = condScope(condRes)
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 5a0f24812dc038484c5d3a5e991d008d965d1190..5d154854f56038d8317b08abb0ce3e3d1f05fce1 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -3,12 +3,11 @@
package leon
package xlang
-import leon.purescala.Definitions._
-import leon.verification._
+import purescala.Definitions.Program
+import purescala.FunctionClosure
+import verification._
-import leon.utils._
-
-object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
+object XLangAnalysisPhase extends TransformationPhase {
val name = "xlang analysis"
val description = "apply analysis on xlang"
@@ -20,72 +19,12 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
case object InvariantInd extends VCKind("invariant inductive", "inv. ind.")
}
- def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
-
+ def apply(ctx: LeonContext, pgm: Program): Program = {
ArrayTransformation(ctx, pgm) // In-place
EpsilonElimination(ctx, pgm) // In-place
- val pgm1 = ImperativeCodeElimination.run(ctx)(pgm)
- val pgm2 = purescala.FunctionClosure.run(ctx)(pgm1)
-
- if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
- PrintTreePhase("Program after xlang transformations").run(ctx)(pgm2)
- }
-
- val subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
-
- val newOptions = ctx.options map {
- case LeonOption(SharedOptions.optFunctions, fs) => {
- var freshToAnalyse: Set[String] = Set()
- fs.asInstanceOf[Seq[String]].foreach((toAnalyse: String) => {
- pgm.definedFunctions.find(_.id.name == toAnalyse) match {
- case Some(fd) => {
- val children = subFunctionsOf(fd)
- freshToAnalyse ++= children.map(_.id.name)
- freshToAnalyse += fd.id.name
- }
- case None =>
- }
- })
-
- LeonOption(SharedOptions.optFunctions)(freshToAnalyse.toList)
- }
- case opt => opt
- }
-
- val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm2)
- completeVerificationReport(vr)
+ (ImperativeCodeElimination andThen FunctionClosure).run(ctx)(pgm)
}
- def completeVerificationReport(vr: VerificationReport): VerificationReport = {
- //this is enough to convert invariant postcondition and inductive conditions. However the initial validity
- //of the invariant (before entering the loop) will still appear as a regular function precondition
- //To fix this, we need some information in the VCs about which function the precondtion refers to
- //although we could arguably say that the term precondition is general enough to refer both to a loop invariant
- //precondition and a function invocation precondition
-
- val newResults = for ((vc, ovr) <- vr.results) yield {
- val (vcKind, fd) = vc.fd.flags.collectFirst { case IsLoop(orig) => orig } match {
- case None => (vc.kind, vc.fd)
- case Some(owner) => (vc.kind.underlying match {
- case VCKinds.Precondition => VCXLangKinds.InvariantInd
- case VCKinds.Postcondition => VCXLangKinds.InvariantPost
- case _ => vc.kind
- }, owner)
- }
-
- val nvc = VC(
- vc.condition,
- fd,
- vcKind,
- vc.tactic
- ).setPos(vc.getPos)
-
- nvc -> ovr
-
- }
-
- VerificationReport(newResults)
- }
}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationSuite.scala b/src/test/scala/leon/test/verification/XLangVerificationSuite.scala
index 7cb6c0ab99e7021dcdfb8bb21d0cd123840329b1..aee24688750fd1547bf4f70f671efbd7d98cdcf4 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationSuite.scala
@@ -5,8 +5,8 @@ package leon.test.verification
import leon._
import leon.test._
-import leon.verification.VerificationReport
-import leon.xlang.XLangAnalysisPhase
+import leon.verification.{AnalysisPhase, VerificationReport}
+import leon.xlang.{FixReportLabels, XLangAnalysisPhase}
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
@@ -25,7 +25,9 @@ class XLangVerificationSuite extends LeonTestSuite {
private def mkPipeline : Pipeline[List[String],VerificationReport] =
ExtractionPhase andThen
PreprocessingPhase andThen
- XLangAnalysisPhase
+ XLangAnalysisPhase andThen
+ AnalysisPhase andThen
+ FixReportLabels
private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath
@@ -103,7 +105,6 @@ class XLangVerificationSuite extends LeonTestSuite {
"There should be at least one invalid verification condition.")
assert(report.totalUnknown === 0,
"There should not be unknown verification conditions.")
- assert(reporter.errorCount >= report.totalInvalid)
}
}