From f7d5492923cf49d258e7a62e0254e7e046d24752 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 28 May 2015 17:35:57 +0200
Subject: [PATCH] re-introduce loop invariants positions
---
src/main/scala/leon/purescala/FunctionClosure.scala | 2 +-
src/main/scala/leon/xlang/ImperativeCodeElimination.scala | 8 +++++---
src/main/scala/leon/xlang/XLangAnalysisPhase.scala | 2 +-
3 files changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 63529f34a..61e6af5c5 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -78,7 +78,7 @@ object FunctionClosure extends TransformationPhase {
val newPrecondition = simplifyLets(introduceLets(and((capturedConstraints ++ fd.precondition).toSeq :_*), fd2FreshFd))
newFunDef.precondition = if(newPrecondition == BooleanLiteral(true)) None else Some(newPrecondition)
- val freshPostcondition = fd.postcondition.map{ post => introduceLets(post, fd2FreshFd) }
+ val freshPostcondition = fd.postcondition.map{ post => introduceLets(post, fd2FreshFd).setPos(post) }
newFunDef.postcondition = freshPostcondition
pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 7b340a12a..a4d8b18c2 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -181,9 +181,11 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
whileFunDef.precondition = invariantPrecondition
whileFunDef.postcondition = trivialPostcondition.map(expr =>
Lambda(Seq(ValDef(resVar.id)), and(expr, invariantPostcondition match {
- case Some(e) => e
- case None => BooleanLiteral(true)
- })))
+ case Some(e) => e
+ case None => BooleanLiteral(true)
+ }).setPos(wh)
+ ).setPos(wh)
+ )
val finalVars = modifiedVars.map(_.freshen)
val finalScope = (body: Expr) => {
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index f6d535767..28ff7349b 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -87,7 +87,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
case VCKinds.Precondition => VCXLangKinds.InvariantInd
case _ => vc.kind
},
- vc.tactic)
+ vc.tactic).setPos(vc.getPos)
nvc -> ovr
} else {
--
GitLab