From 8f488a11114e123dac68433df064decfc6baf541 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 05:52:52 +0000
Subject: [PATCH] fix bug in testcase and support the complete language in
ArrayTransformation
---
src/main/scala/leon/ArrayTransformation.scala | 18 ++++++++++++++++--
testcases/regression/valid/Array4.scala | 12 ++++++++++--
2 files changed, 26 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index a61605287..d25965ede 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -116,9 +116,23 @@ object ArrayTransformation extends Pass {
LetVar(id, er, br)
}
- //case ite@IfExpr(cond, tExpr, eExpr) =>
+ case ite@IfExpr(c, t, e) => {
+ val rc = transform(c)
+ val rt = transform(t)
+ val re = transform(e)
+ IfExpr(rc, rt, re).setType(rt.getType)
+ }
+
+ case m @ MatchExpr(scrut, cses) => {
+ val scrutRec = transform(scrut)
+ val csesRec = cses.map{
+ case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+ case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+ }
+ val tpe = csesRec.head.rhs.getType
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ }
- //case m @ MatchExpr(scrut, cses) =>
//case LetDef(fd, b) =>
case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
diff --git a/testcases/regression/valid/Array4.scala b/testcases/regression/valid/Array4.scala
index 479f243ba..fd76e02fa 100644
--- a/testcases/regression/valid/Array4.scala
+++ b/testcases/regression/valid/Array4.scala
@@ -1,7 +1,15 @@
+import leon.Utils._
+
object Array4 {
def foo(a: Array[Int]): Int = {
- a(2)
- } ensuring(_ == 3)
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
}
--
GitLab