From c6ec95788f0bbd0c66517fe6a4a49ab278e3e2d2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 6 Apr 2016 18:40:49 +0200
Subject: [PATCH] xlang does not lift code outside of lambdas
---
.../leon/xlang/ImperativeCodeElimination.scala | 5 +++++
.../verification/xlang/valid/Lambda1.scala | 13 +++++++++++++
2 files changed, 18 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/Lambda1.scala
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index de75b7a29..3636fd6e5 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -304,6 +304,11 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
}
}
+ //TODO: handle vars in scope, just like LetDef
+ case ld@Lambda(params, body) =>
+ val (bodyVal, bodyScope, bodyFun) = toFunction(body)
+ (Lambda(params, bodyScope(bodyVal)).copiedFrom(ld), (e: Expr) => e, Map())
+
case c @ Choose(b) =>
//Recall that Choose cannot mutate variables from the scope
(c, (b2: Expr) => b2, Map())
diff --git a/src/test/resources/regression/verification/xlang/valid/Lambda1.scala b/src/test/resources/regression/verification/xlang/valid/Lambda1.scala
new file mode 100644
index 000000000..b228f96f7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Lambda1.scala
@@ -0,0 +1,13 @@
+object Lambda1 {
+
+ def test(): Int = {
+ val x = 2
+ val cl = ((y: Int) => {
+ var z = y
+ z = z + x
+ z
+ })
+ cl(4)
+ } ensuring(_ == 6)
+
+}
--
GitLab