diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 40cd6c23fbeb39130cad5a7bf829c8931fa3f30e..da28a90d50d989c02e31aae2c900a1e59e69ce5d 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -40,5 +40,6 @@ case class LeonValueOptionDef(name: String, usageOption: String, usageDesc: Stri
}
object ListValue {
+ def apply(values: Seq[String]) = values.mkString(":")
def unapply(value: String): Option[Seq[String]] = Some(value.split(':').map(_.trim).filter(!_.isEmpty))
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 26477afd3a2f5227039cf4f7ae3034d14cdeac0d..56d66e6019c5fea40c9fd382e617f66befa44f86 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -9,6 +9,7 @@ object Main {
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
xlang.FunctionClosure,
+ xlang.XlangAnalysisPhase,
synthesis.SynthesisPhase,
verification.AnalysisPhase
)
@@ -118,16 +119,6 @@ object Main {
val pipeBegin : Pipeline[List[String],Program] = plugin.ExtractionPhase
- val pipeTransforms: Pipeline[Program, Program] =
- if (settings.xlang) {
- xlang.ArrayTransformation andThen
- xlang.EpsilonElimination andThen
- xlang.ImperativeCodeElimination andThen
- xlang.FunctionClosure
- } else {
- NoopPhase()
- }
-
val pipeSynthesis: Pipeline[Program, Program]=
if (settings.synthesis) {
synthesis.SynthesisPhase
@@ -136,14 +127,15 @@ object Main {
}
val pipeVerify: Pipeline[Program, Any] =
- if (settings.verify) {
+ if (settings.xlang) {
+ xlang.XlangAnalysisPhase
+ } else if (settings.verify) {
verification.AnalysisPhase
} else {
NoopPhase()
}
pipeBegin andThen
- pipeTransforms andThen
pipeSynthesis andThen
pipeVerify
}
@@ -159,7 +151,10 @@ object Main {
try {
// Run pipeline
- pipeline.run(ctx)(args.toList)
+ pipeline.run(ctx)(args.toList) match {
+ case (report: verification.VerificationReport) => reporter.info(report.summaryString)
+ case _ =>
+ }
} catch {
case LeonFatalError() => sys.exit(1)
}
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
index 08291badcd2dca0f6945bdf7c330493bef53c2fe..41cda6b80a462276cc0b026bb9423b4a7be40919 100644
--- a/src/main/scala/leon/TypeChecking.scala
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -87,8 +87,6 @@ object TypeChecking extends UnitPhase[Program] {
// val freshFunName = FreshIdentifier(fd.id.name)
// val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
// fd2fd += (fd -> freshFunDef)
- // freshFunDef.fromLoop = fd.fromLoop
- // freshFunDef.parent = fd.parent
// freshFunDef.precondition = fd.precondition.map(transform)
// freshFunDef.postcondition = fd.postcondition.map(transform)
// freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 3d56d537723f5286c950d50bdc84b755d3715180..dc58a24bed859b7aa860940ca7d46be04219ae3d 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -23,8 +23,6 @@ object UnitElimination extends TransformationPhase {
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.args.exists(vd => vd.tpe == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
- freshFunDef.fromLoop = fd.fromLoop
- freshFunDef.parent = fd.parent
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
@@ -102,8 +100,6 @@ object UnitElimination extends TransformationPhase {
val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
- freshFunDef.parent = fd.parent
- freshFunDef.fromLoop = fd.fromLoop
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
fun2FreshFun += (fd -> freshFunDef)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 6eee2247c7792a4653fe5fdbb541bb5fc4f023b2..80f1df9843c89bb258483d177bb159238e2fe69b 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -313,11 +313,6 @@ object Definitions {
var precondition: Option[Expr] = None
var postcondition: Option[Expr] = None
- //true if this function has been generated from a while loop
- var fromLoop = false
- //the fundef where the loop was defined (if applies)
- var parent: Option[FunDef] = None
-
def hasImplementation : Boolean = body.isDefined
def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2e340cac1e6f8db1abd2efef32e7ef27a147e8b7..146f8bb2d94e6dd4f1e64395671680f188f69f12 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -148,7 +148,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
val report = new VerificationReport(vcs)
- reporter.info(report.summaryString)
report
}
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 47a2af0d2a098722e36af1c2e829bf31e5734a59..cdc752a50930dc3cecd6230a7555cf998371ea0b 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -44,10 +44,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrec
}
- if(functionDefinition.fromLoop)
- Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
- else
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
}
}
@@ -76,13 +73,13 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
val newBody : Expr = replace(substMap, prec)
val newCall : Expr = (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e))
- if(fd.fromLoop)
- new VerificationCondition(
- withPrecIfDefined(path, newCall),
- fd.parent.get,
- if(fd == function) VCKind.InvariantInd else VCKind.InvariantInit,
- this.asInstanceOf[DefaultTactic]).setPosInfo(fd)
- else
+ //if(fd.fromLoop)
+ // new VerificationCondition(
+ // withPrecIfDefined(path, newCall),
+ // fd.parent.get,
+ // if(fd == function) VCKind.InvariantInd else VCKind.InvariantInit,
+ // this.asInstanceOf[DefaultTactic]).setPosInfo(fd)
+ //else
new VerificationCondition(
withPrecIfDefined(path, newCall),
function,
@@ -117,7 +114,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- if(function.fromLoop) function.parent.get else function,
+ function,//if(function.fromLoop) function.parent.get else function,
VCKind.ExhaustiveMatch,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
@@ -149,7 +146,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- if(function.fromLoop) function.parent.get else function,
+ function, //if(function.fromLoop) function.parent.get else function,
VCKind.MapAccess,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
@@ -178,7 +175,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
allPathConds.map(pc =>
new VerificationCondition(
withPrecIfDefined(pc._1),
- if(function.fromLoop) function.parent.get else function,
+ function, //if(function.fromLoop) function.parent.get else function,
VCKind.ArrayAccess,
this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
).toSeq
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 573bcd6992a1dfcabc4232e7af3d4db46c5469fe..893fb39b3a0cbd22485f1fb0d10230d8cb8fd2b9 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -42,4 +42,5 @@ object VCKind extends Enumeration {
val InvariantInit = Value("inv init.")
val InvariantInd = Value("inv ind.")
val InvariantPost = Value("inv post.")
+ val InvariantPre = Value("inv pre.")
}
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 880e870f52134dccd7b7ddd3397fe86b01b3cf53..4a9017597ff67ecee4a0d5f9c7972afc37ab564f 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -142,8 +142,6 @@ object ArrayTransformation extends TransformationPhase {
// val freshFunName = FreshIdentifier(fd.id.name)
// val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
// fd2fd += (fd -> freshFunDef)
- // freshFunDef.fromLoop = fd.fromLoop
- // freshFunDef.parent = fd.parent
// freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
// freshFunDef
// } else fd
@@ -272,8 +270,6 @@ object ArrayTransformation extends TransformationPhase {
// val freshFunName = FreshIdentifier(fd.id.name)
// val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
// fd2fd += (fd -> freshFunDef)
- // freshFunDef.fromLoop = fd.fromLoop
- // freshFunDef.parent = fd.parent
// freshFunDef.precondition = fd.precondition.map(transform)
// freshFunDef.postcondition = fd.postcondition.map(transform)
// freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index 47e0cbeede0090b6afc8e784ed127943d7e12177..c6fc16e1f785867c3b54a7f2da2ae87313b2f791 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/src/main/scala/leon/xlang/FunctionClosure.scala
@@ -1,4 +1,5 @@
-package leon.xlang
+package leon
+package xlang
import leon.TransformationPhase
import leon.LeonContext
@@ -10,31 +11,41 @@ import leon.purescala.TreeOps._
import leon.purescala.TypeTrees._
import leon.xlang.Trees._
-object FunctionClosure extends TransformationPhase{
+object FunctionClosure extends LeonPhase[Program, (Program, Map[FunDef, FunDef], Map[FunDef, FunDef])] {
val name = "Function Closure"
val description = "Closing function with its scoping variables"
+ /* I know, that's a lot of mutable variables */
private var pathConstraints: List[Expr] = Nil
private var enclosingLets: List[(Identifier, Expr)] = Nil
private var newFunDefs: Map[FunDef, FunDef] = Map()
private var topLevelFuns: Set[FunDef] = Set()
+ private var parent: FunDef = null //refers to the current toplevel parent
+ private var parents: Map[FunDef, FunDef] = null //each hoisted function mapped to its original parent
+ private var freshFunDefs: Map[FunDef, FunDef] = null //mapping from original FunDef in LetDef to the fresh ones
+ /* but notice the private keyword */
- def apply(ctx: LeonContext, program: Program): Program = {
+ //return modified program, new funDef to their original parents, old FunDef to freshly introduced FunDef
+ def run(ctx: LeonContext)(program: Program): (Program, Map[FunDef, FunDef], Map[FunDef, FunDef]) = {
pathConstraints = Nil
enclosingLets = Nil
newFunDefs = Map()
topLevelFuns = Set()
+ parent = null
+ parents = Map()
+ freshFunDefs = Map()
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
+ parent = fd
pathConstraints = fd.precondition.toList
fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet, Map(), Map()))
})
val Program(id, ObjectDef(objId, defs, invariants)) = program
val res = Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
- res
+ (res, parents, freshFunDefs)
}
private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
@@ -50,13 +61,13 @@ object FunctionClosure extends TransformationPhase{
val extraVarDecls: Seq[VarDecl] = extraVarDeclFreshIds.map(id => VarDecl(id, id.getType))
val newVarDecls: Seq[VarDecl] = fd.args ++ extraVarDecls
val newBindedVars: Set[Identifier] = bindedVars ++ fd.args.map(_.id)
- val newFunId = FreshIdentifier(fd.id.name)
+ val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPosInfo(fd)
topLevelFuns += newFunDef
- newFunDef.fromLoop = fd.fromLoop
- newFunDef.parent = fd.parent
- newFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
+ parents += (newFunDef -> parent)
+ freshFunDefs += (fd -> newFunDef)
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/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index b926893cdbecd03b17cf85113fc60171cf6783f9..656104b92307f81cf9576fb57d2ecd15a82b7a80 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -1,4 +1,5 @@
-package leon.xlang
+package leon
+package xlang
import leon.TransformationPhase
import leon.LeonContext
@@ -10,16 +11,18 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
import leon.xlang.Trees._
-object ImperativeCodeElimination extends TransformationPhase {
+object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef])] {
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
+ private var wasLoop: Set[FunDef] = null //record FunDef that are the transformation of loops
- def apply(ctx: LeonContext, pgm: Program): Program = {
+ def run(ctx: LeonContext)(pgm: Program): (Program, Set[FunDef]) = {
varInScope = Set()
+ wasLoop = Set()
parent = null
val allFuns = pgm.definedFunctions
@@ -28,7 +31,7 @@ object ImperativeCodeElimination extends TransformationPhase {
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
}))
- pgm
+ (pgm, wasLoop)
}
//return a "scope" consisting of purely functional code that defines potentially needed
@@ -150,9 +153,8 @@ object ImperativeCodeElimination extends TransformationPhase {
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunVarDecls = whileFunVars.map(id => VarDecl(id, id.getType))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(FreshIdentifier("while"), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
- whileFunDef.fromLoop = true
- whileFunDef.parent = Some(parent)
+ val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
+ wasLoop += whileFunDef
val whileFunCond = condRes
val whileFunRecursiveCall = replaceNames(condFun,
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 31c717784281d5bf556580d6c9cf77b9a23cbec1..13fded9dc87ac2b3635b1c045acda927ab01227e 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -261,8 +261,6 @@ object Trees {
case (None, None) =>
Some((Seq(b, body), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//LetDef(nfd, as(1))
fd.body = Some(as(0))
@@ -271,8 +269,6 @@ object Trees {
case (Some(pre), None) =>
Some((Seq(b, body, pre), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//nfd.precondition = Some(as(2))
//LetDef(nfd, as(1))
@@ -283,8 +279,6 @@ object Trees {
case (None, Some(post)) =>
Some((Seq(b, body, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//nfd.postcondition = Some(as(2))
//LetDef(nfd, as(1))
@@ -295,8 +289,6 @@ object Trees {
case (Some(pre), Some(post)) =>
Some((Seq(b, body, pre, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.body = Some(as(0))
//nfd.precondition = Some(as(2))
//nfd.postcondition = Some(as(3))
@@ -313,16 +305,12 @@ object Trees {
case (None, None) =>
Some((Seq(body), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//LetDef(nfd, as(0))
LetDef(fd, as(0))
}))
case (Some(pre), None) =>
Some((Seq(body, pre), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.precondition = Some(as(1))
//LetDef(nfd, as(0))
fd.precondition = Some(as(1))
@@ -331,8 +319,6 @@ object Trees {
case (None, Some(post)) =>
Some((Seq(body, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.postcondition = Some(as(1))
//LetDef(nfd, as(0))
fd.postcondition = Some(as(1))
@@ -341,8 +327,6 @@ object Trees {
case (Some(pre), Some(post)) =>
Some((Seq(body, pre, post), (as: Seq[Expr]) => {
//val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- //nfd.fromLoop = fd.fromLoop
- //nfd.parent = fd.parent
//nfd.precondition = Some(as(1))
//nfd.postcondition = Some(as(2))
//LetDef(nfd, as(0))
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f29e272fe66453c8389f5bd8f827238db71bdc1
--- /dev/null
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -0,0 +1,80 @@
+package leon
+package xlang
+
+import leon.purescala.Definitions._
+import leon.verification._
+
+object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
+
+ val name = "xlang analysis"
+ val description = "apply analysis on xlang"
+
+ def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
+
+ val pgm1 = ArrayTransformation(ctx, pgm)
+ val pgm2 = EpsilonElimination(ctx, pgm1)
+ val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
+ val (pgm4, parents, freshFunDefs) = FunctionClosure.run(ctx)(pgm3)
+
+ val originalFunDefs = freshFunDefs.map(x => (x._2, x._1))
+
+ def functionWasLoop(fd: FunDef): Boolean = originalFunDefs.get(fd) match {
+ case None => false //meaning, this was a top level function
+ case Some(nested) => wasLoop.contains(nested) //could have been a LetDef originally
+ }
+ def subFunctionsOf(fd: FunDef): Set[FunDef] = parents.flatMap((p: (FunDef, FunDef)) => p match {
+ case (child, parent) => if(parent == fd) List(child) else List()
+ }).toSet
+
+ val newOptions = ctx.options map {
+ case LeonValueOption("functions", ListValue(fs)) => {
+ var freshToAnalyse: Set[String] = Set()
+ fs.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 =>
+ }
+ })
+
+ LeonValueOption("functions", ListValue(freshToAnalyse.toList))
+ }
+ case opt => opt
+ }
+ val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
+ val vcs = vr.conditions
+
+ //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 freshVcs = vcs.map(vc => {
+ val funDef = vc.funDef
+ if(functionWasLoop(funDef)) {
+ val freshVc = new VerificationCondition(
+ vc.condition,
+ parents(funDef),
+ if(vc.kind == VCKind.Postcondition) VCKind.InvariantPost else if(vc.kind == VCKind.Precondition) VCKind.InvariantInd else vc.kind,
+ vc.tactic,
+ vc.info).setPosInfo(funDef)
+ freshVc.value = vc.value
+ freshVc.solvedWith = vc.solvedWith
+ freshVc.time = vc.time
+ freshVc
+ } else vc
+ })
+
+ val sortedFreshVcs = freshVcs.sortWith((vc1, vc2) => {
+ val id1 = vc1.funDef.id.name
+ val id2 = vc2.funDef.id.name
+ if(id1 != id2) id1 < id2 else vc1 < vc2
+ })
+
+ new VerificationReport(sortedFreshVcs)
+ }
+
+}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 4102f5b87ed3185ab4b60492351a151aee698bbc..f5b33c3e21d256f995a135cf9c56880a3c4f31ac 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -19,12 +19,7 @@ class XLangVerificationRegression extends FunSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.plugin.ExtractionPhase andThen
- xlang.ArrayTransformation andThen
- xlang.EpsilonElimination andThen
- xlang.ImperativeCodeElimination andThen
- xlang.FunctionClosure andThen
- leon.verification.AnalysisPhase
+ leon.plugin.ExtractionPhase andThen xlang.XlangAnalysisPhase
private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
val fullName = file.getPath()