From d47515b8b7b4fbcfc19ccade8ca0e767125a3010 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 23 Oct 2015 13:18:28 +0200
Subject: [PATCH] fix
---
.../leon/xlang/ImperativeCodeElimination.scala | 4 ++--
.../xlang/valid/FunInvocEvaluationOrder3.scala | 17 +++++++++++++++++
2 files changed, 19 insertions(+), 2 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 989942f22..7ab5925ce 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -242,7 +242,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val fd = tfd.fd
state.funDefsMapping.get(fd) match {
case Some((newFd, modifiedVars)) => {
- val newInvoc = FunctionInvocation(newFd.typed, args ++ modifiedVars.map(id => id.toVariable)).setPos(fi)
+ val newInvoc = FunctionInvocation(newFd.typed, recArgs ++ modifiedVars.map(id => id.toVariable)).setPos(fi)
val freshNames = modifiedVars.map(id => id.freshen)
val tmpTuple = FreshIdentifier("t", newFd.returnType)
@@ -252,7 +252,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
Let(p._1, TupleSelect(tmpTuple.toVariable, p._2 + 2), b))
))
}
- val newMap = modifiedVars.zip(freshNames).toMap ++ argFun
+ val newMap = argFun ++ modifiedVars.zip(freshNames).toMap
(TupleSelect(tmpTuple.toVariable, 1), scope, newMap)
}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
new file mode 100644
index 000000000..f26352965
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
@@ -0,0 +1,17 @@
+object FunInvocEvaluationOrder3 {
+
+ def leftToRight(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def nested(x: BigInt, y: BigInt): Unit = {
+ a = x + y
+ }
+
+ nested({a += 10; a}, {a *= 2; a})
+ a
+
+ } ensuring(_ == 30)
+
+}
--
GitLab