From d6322dc8fc95c8fdc7352b2abbb9b896d2e82c7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 08:37:37 +0000
Subject: [PATCH] difficult example with copy array, that does not work well
---
src/main/scala/leon/ArrayTransformation.scala | 15 ++++++++++-----
testcases/regression/valid/Array7.scala | 17 +++++++++++++++++
2 files changed, 27 insertions(+), 5 deletions(-)
create mode 100644 testcases/regression/valid/Array7.scala
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 3927d1ff9..09fcec912 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -19,7 +19,7 @@ object ArrayTransformation extends Pass {
val newFuns: Seq[FunDef] = allFuns.map(fd => {
if(fd.hasImplementation) {
val args = fd.args
- if(args.exists(vd => containsArrayType(vd.tpe))) {
+ if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
val newArgs = args.map(vd => {
val freshId = FreshIdentifier(vd.id.name).setType(TupleType(Seq(vd.tpe, Int32Type)))
id2id += (vd.id -> freshId)
@@ -27,7 +27,7 @@ object ArrayTransformation extends Pass {
VarDecl(freshId, newTpe)
})
val freshFunName = FreshIdentifier(fd.id.name)
- val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
+ val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
freshFunDef.fromLoop = fd.fromLoop
freshFunDef.parent = fd.parent
freshFunDef.precondition = fd.precondition.map(transform)
@@ -69,7 +69,7 @@ object ArrayTransformation extends Pass {
var rLength = transform(length)
val rDefault = transform(default)
val rFill = ArrayMake(rDefault).setType(fill.getType)
- Tuple(Seq(rFill, length)).setType(TupleType(Seq(fill.getType, Int32Type)))
+ Tuple(Seq(rFill, rLength)).setType(TupleType(Seq(fill.getType, Int32Type)))
}
case sel@ArraySelect(a, i) => {
val ar = transform(a)
@@ -126,6 +126,11 @@ object ArrayTransformation extends Pass {
val br = transform(b)
LetVar(id, er, br)
}
+ case wh@While(c, e) => {
+ val newWh = While(transform(c), transform(e))
+ newWh.invariant = wh.invariant.map(i => transform(i))
+ newWh.setPosInfo(wh)
+ }
case ite@IfExpr(c, t, e) => {
val rc = transform(c)
@@ -148,7 +153,7 @@ object ArrayTransformation extends Pass {
val body = fd.body.get
val args = fd.args
val newFd =
- if(args.exists(vd => containsArrayType(vd.tpe))) {
+ if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
val newArgs = args.map(vd => {
val freshId = FreshIdentifier(vd.id.name).setType(TupleType(Seq(vd.tpe, Int32Type)))
id2id += (vd.id -> freshId)
@@ -156,7 +161,7 @@ object ArrayTransformation extends Pass {
VarDecl(freshId, newTpe)
})
val freshFunName = FreshIdentifier(fd.id.name)
- val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
+ val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
freshFunDef.fromLoop = fd.fromLoop
freshFunDef.parent = fd.parent
freshFunDef.precondition = fd.precondition.map(transform)
diff --git a/testcases/regression/valid/Array7.scala b/testcases/regression/valid/Array7.scala
new file mode 100644
index 000000000..55bbbb729
--- /dev/null
+++ b/testcases/regression/valid/Array7.scala
@@ -0,0 +1,17 @@
+import leon.Utils._
+
+object Array7 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length > 0)
+ val a2 = Array.fill(a.length)(0)
+ var i = 0
+ (while(i < a.length) {
+ a2(i) = a(i)
+ i = i + 1
+ }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true))
+ a2
+ } ensuring(_(0) == a(0))
+
+
+}
--
GitLab