From 43c307c503c7bb62155803ccccab8fa57e6bae7d Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 14 Oct 2015 19:03:40 +0200
Subject: [PATCH] pre and post of nested functions can refer local variables
---
.../leon/xlang/ImperativeCodeElimination.scala | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index cdd2d2722..8726a02a6 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -299,6 +299,21 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val newBody = fdScope(newRes)
newFd.body = Some(newBody)
+ newFd.precondition = fd.precondition.map(prec => {
+ replace(modifiedVars.zip(freshNames).map(p => (p._1.toVariable, p._2.toVariable)).toMap, prec)
+ })
+ newFd.postcondition = fd.postcondition.map(post => {
+ val Lambda(Seq(res), postBody) = post
+ val newRes = ValDef(FreshIdentifier(res.id.name, newFd.returnType))
+
+ val newBody =
+ replace(
+ modifiedVars.zipWithIndex.map{ case (v, i) =>
+ (v.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap +
+ (res.toVariable -> TupleSelect(newRes.toVariable, 1)),
+ postBody)
+ Lambda(Seq(newRes), newBody)
+ })
val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withFunDef(fd, newFd, modifiedVars))
(bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)).copiedFrom(expr), bodyFun)
--
GitLab