diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index d7efcaecf8557e31fab4b61ab04fe17384236718..c5de9b19ae00d3f9ff24090e8df998bd28edcd91 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -75,6 +75,7 @@ class Analysis(pgm : Program, val reporter: Reporter = Settings.reporter) {
allVCs ++= tactic.generatePostconditions(funDef).sortWith(vcSort)
allVCs ++= tactic.generateMiscCorrectnessConditions(funDef).sortWith(vcSort)
}
+ allVCs = allVCs.sortWith((vc1, vc2) => (vc1.funDef.id.name < vc2.funDef.id.name)).sortWith(vcSort)
}
val notFound: Set[String] = Settings.functionsToAnalyse -- analysedFunctions
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
index 6f31b9ff59bc4b4681e7284c4dc3479400585534..d1310e3399d2347cbab52277f3a4d487ad9c6ae7 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -78,7 +78,12 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
expr2
}
}
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ println("generating post condtion with: " + functionDefinition.fromLoop)
+ println("for" + functionDefinition)
+ 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]))
}
}
@@ -107,11 +112,18 @@ 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))
- new VerificationCondition(
- withPrecIfDefined(path, newCall),
- function,
- VCKind.Precondition,
- this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
+ 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,
+ VCKind.Precondition,
+ this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
}).toSeq
} else {
Seq.empty
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index f21f1ad9feb26fba7007444f3f97f82acf66b4ce..f4ec3f1b0fd564113972e687d3082904d46eb050 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -48,6 +48,8 @@ object FunctionClosure extends Pass {
val newVarDecls = varDecl ++ extraVarDecls
val newFunId = FreshIdentifier(id.name)
val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
+ newFunDef.fromLoop = fd.fromLoop
+ newFunDef.parent = fd.parent
val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index 9c21a5d2a1e3eeda42386b39f835866488ef9872..b006520ebd0eee5b1d49861534d5dc686f8dea57 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -10,10 +10,12 @@ object ImperativeCodeElimination extends Pass {
val description = "Transform imperative constructs into purely functional code"
private var varInScope = Set[Identifier]()
+ private var parent: FunDef = null //the enclosing fundef
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
+ parent = fd
val (res, scope, _) = toFunction(fd.getBody)
fd.body = Some(scope(res))
})
@@ -140,10 +142,12 @@ object ImperativeCodeElimination extends Pass {
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 whileFunCond = condRes
val whileFunRecursiveCall = replaceNames(condFun,
- bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable))))
+ bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable)).setPosInfo(wh)))
val whileFunBaseCase =
(if(whileFunVars.size == 1)
condFun.get(modifiedVars.head).getOrElse(whileFunVars.head).toVariable
@@ -182,7 +186,7 @@ object ImperativeCodeElimination extends Pass {
LetDef(
whileFunDef,
Let(tupleId,
- FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)),
+ FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)).setPosInfo(wh),
if(finalVars.size == 1)
Let(finalVars.head, tupleId.toVariable, body)
else
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index b52561750f4a6fab8327c4bdd6862e96d2f24bb6..7fe181fba57f7c80d0aa878896641b8195742485 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -20,6 +20,8 @@ object UnitElimination extends Pass {
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..
fun2FreshFun += (fd -> freshFunDef)
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
index 4150536fa441352761a7542019caa64d478b0d6a..01545bc3e87bd3606591b464f59098a5b0d8dd8c 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -49,4 +49,7 @@ object VCKind extends Enumeration {
val Postcondition = Value("postcond.")
val ExhaustiveMatch = Value("match.")
val MapAccess = Value("map acc.")
+ val InvariantInit = Value("inv init.")
+ val InvariantInd = Value("inv ind.")
+ val InvariantPost = Value("inv post.")
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index efd8b52fb31e7cd4d61ff868bba3c836ca1f0e2e..f2da8a7cef1f1f3b0290a35a260f40ceefbf6705 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -283,6 +283,11 @@ 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