From 7a5125138456e210fb47a1301e80e38542f594e2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 28 May 2015 16:51:40 +0200
Subject: [PATCH] fix while loop with complicated conditions
---
.../xlang/ImperativeCodeElimination.scala | 2 +-
.../valid/WhileConditionSubexpression.scala | 20 +++++++++++++++++++
2 files changed, 21 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 8f26df8f4..7b340a12a 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -155,7 +155,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs,DefType.MethodDef).setPos(wh)
wasLoop += whileFunDef
- val whileFunCond = condRes
+ val whileFunCond = condScope(condRes)
val whileFunRecursiveCall = replaceNames(condFun,
bodyScope(FunctionInvocation(whileFunDef.typed, modifiedVars.map(id => condBodyFun(id).toVariable)).setPos(wh)))
val whileFunBaseCase =
diff --git a/src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala b/src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala
new file mode 100644
index 000000000..b57fc9d8b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+import leon.lang._
+
+object WhileConditionSubexpression {
+
+ def test(x: Int): Boolean = {
+ var b = false
+ var i = 0
+ while(!b && i < 10) {
+ if(i == x)
+ b = true
+ i += 1
+ }
+ b
+ } ensuring(res => res || (x != 0 && x != 1 && x != 2))
+
+}
--
GitLab