From 7fe931bf7460460b18d605e4cc7f74cf0a6006ef Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 14 Sep 2015 12:08:25 +0200
Subject: [PATCH] Treat function invocations in XLang correctly
---
.../xlang/ImperativeCodeElimination.scala | 22 +++++++++----------
1 file changed, 10 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index b1aa75ea3..bbda600a4 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -188,7 +188,16 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val (scope, fun) = exprs.foldRight((body: Expr) => body, Map[Identifier, Identifier]())((e, acc) => {
val (accScope, accFun) = acc
val (_, rScope, rFun) = toFunction(e)
- val scope = (body: Expr) => rScope(replaceNames(rFun, accScope(body)))
+ val scope = (body: Expr) => {
+ val withoutPrec = rScope(replaceNames(rFun, accScope(body)))
+ e match {
+ case FunctionInvocation(tfd, args) if tfd.hasPrecondition =>
+ Assert(tfd.withParamSubst(args, tfd.precondition.get), Some("Precondition failed"), withoutPrec)
+ case _ =>
+ withoutPrec
+ }
+
+ }
(scope, rFun ++ accFun)
})
val (lastRes, lastScope, lastFun) = toFunction(expr)
@@ -222,17 +231,6 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
//Recall that Choose cannot mutate variables from the scope
(c, (b2: Expr) => b2, Map())
- case i @ FunctionInvocation(fd, args) =>
- //function invocation can have side effects so we should keep them as local
- //val names.
- val scope =
- (body: Expr) => Let(
- FreshIdentifier("tmp", fd.returnType),
- i,
- body
- )
- (i, scope, Map())
-
case And(args) =>
val ifExpr = args.reduceRight((el, acc) => IfExpr(el, acc, BooleanLiteral(false)))
toFunction(ifExpr)
--
GitLab