From 6f808f72f3a668e6c00979ff1d3ec1dd37bb1346 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 16 Apr 2013 16:54:32 +0200
Subject: [PATCH] Fix choose with imperative phase
Choose was introduced after imperative transformation
and was not adapted to the transformation rule.
Since Choose can introduce a scope, val defined
inside its body should not be hoisted outside.
---
.../leon/xlang/ImperativeCodeElimination.scala | 5 +++++
.../verification/xlang/valid/Choose1.scala | 14 ++++++++++++++
2 files changed, 19 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/Choose1.scala
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 656104b92..2daf0696c 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -244,6 +244,11 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val (bodyRes, bodyScope, bodyFun) = toFunction(b)
(bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)), bodyFun)
}
+ case Choose(ids, b) => {
+ //Recall that Choose cannot mutate variables from the scope
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)
+ (bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)), bodyFun)
+ }
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => {
val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
new file mode 100644
index 000000000..702024e96
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
@@ -0,0 +1,14 @@
+import leon.Utils._
+
+object Test {
+
+ def test(x: Int): Int = {
+
+ choose((y: Int) => {
+ val z = y + 2
+ z == y
+ })
+
+ } ensuring(_ == x + 2)
+
+}
--
GitLab