From fb21e0119779532952dc8604c8b42b6379591837 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 29 Mar 2012 02:44:25 +0000
Subject: [PATCH] bad replace of variables in blocks
---
mytest/Assign1.scala | 15 ++++++++----
mytest/Bubble.scala | 24 ++++++++++++++-----
.../leon/ImperativeCodeElimination.scala | 4 ++--
3 files changed, 31 insertions(+), 12 deletions(-)
diff --git a/mytest/Assign1.scala b/mytest/Assign1.scala
index 864eb7bfc..ef346a02c 100644
--- a/mytest/Assign1.scala
+++ b/mytest/Assign1.scala
@@ -1,10 +1,17 @@
object Assign1 {
def foo(): Int = {
- var a = 1
- var b = a
- a = a + 1
- b = b + a
+ var a = 0
+ val tmp = a + 1
+ a = a + 2
+ a = a + 3
+ a = a + 4
+ //var j = 0
+ //var sortedArray = Map.empty[Int, Int]
+ //val tmp = sortedArray(j)
+ //sortedArray = sortedArray.updated(j, sortedArray(j+1))
+ //sortedArray = sortedArray.updated(j+1, tmp)
+ //sortedArray(j)
a
}
diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index 1c6dc98bc..9a1b8fd44 100644
--- a/mytest/Bubble.scala
+++ b/mytest/Bubble.scala
@@ -2,24 +2,36 @@ import leon.Utils._
object Bubble {
- def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = {
- require(isArray(a, size))
+ def sort(a: Map[Int, Int], size: Int, k: Int): Map[Int, Int] = ({
+ require(size > 0 && k < size - 1 && k >= 0)
var i = size - 1
var j = 0
var sortedArray = a
(while(i > 0) {
j = 0
(while(j < i) {
- if(a(j) > a(j+1)) {
+ if(sortedArray(j) > sortedArray(j+1)) {
val tmp = sortedArray(j)
- sortedArray = sortedArray.updated(j, a(j+1))
+ sortedArray = sortedArray.updated(j, sortedArray(j+1))
sortedArray = sortedArray.updated(j+1, tmp)
}
j = j + 1
- }) invariant(isArray(sortedArray, size) && j >= 0 && j <= i && i < size && i >= 0)
+ }) invariant(j >= 0 && j <= i)
i = i - 1
- }) invariant(isArray(sortedArray, size) && i >= 0 && i < size)
+ }) invariant(i >= 0 && i < size && (k < i || sortedArray(k) <= sortedArray(k+1)))
sortedArray
+ }) ensuring(res => res(k) <= res(k+1))
+ //ensuring(res => sorted(res, 0, size-1))
+
+ def sorted(a: Map[Int, Int], l: Int, u: Int): Boolean = {
+ var k = l
+ var sorted = true
+ while(k < u) {
+ if(a(k) > a(k+1))
+ sorted = false
+ k = k + 1
+ }
+ sorted
}
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index f59479c74..b44e21cf4 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -132,8 +132,8 @@ object ImperativeCodeElimination extends Pass {
(scope, accFun ++ rFun)
})
val (lastRes, lastScope, lastFun) = toFunction(expr)
- (replace(fun.map{ case (i1, i2) => (i1.toVariable, i2.toVariable) }, lastRes),
- (body: Expr) => scope(lastScope(body)),
+ (lastRes,
+ (body: Expr) => scope(replace(fun.map{ case (i1, i2) => (i1.toVariable, i2.toVariable) }, lastScope(body))),
fun ++ lastFun)
}
--
GitLab