From e75513ebc42d37f16310a5e926ecf091d8f2ab24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 06:38:29 +0000
Subject: [PATCH] also apply the transformation to precondition and
postcondition
---
src/main/scala/leon/ArrayTransformation.scala | 8 ++++----
testcases/regression/valid/Array5.scala | 2 +-
testcases/regression/valid/Array6.scala | 15 +++++++++++++++
3 files changed, 20 insertions(+), 5 deletions(-)
create mode 100644 testcases/regression/valid/Array6.scala
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 35cad52f2..75ce22ff0 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -30,8 +30,8 @@ object ArrayTransformation extends Pass {
val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
freshFunDef.fromLoop = fd.fromLoop
freshFunDef.parent = fd.parent
- freshFunDef.precondition = fd.precondition
- freshFunDef.postcondition = fd.postcondition
+ freshFunDef.precondition = fd.precondition.map(transform)
+ freshFunDef.postcondition = fd.postcondition.map(transform)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
fd2fd += (fd -> freshFunDef)
freshFunDef
@@ -160,8 +160,8 @@ object ArrayTransformation extends Pass {
val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
freshFunDef.fromLoop = fd.fromLoop
freshFunDef.parent = fd.parent
- freshFunDef.precondition = fd.precondition
- freshFunDef.postcondition = fd.postcondition
+ freshFunDef.precondition = fd.precondition.map(transform)
+ freshFunDef.postcondition = fd.postcondition.map(transform)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
fd2fd += (fd -> freshFunDef)
freshFunDef
diff --git a/testcases/regression/valid/Array5.scala b/testcases/regression/valid/Array5.scala
index 1f36c1a76..14bed6eff 100644
--- a/testcases/regression/valid/Array5.scala
+++ b/testcases/regression/valid/Array5.scala
@@ -1,6 +1,6 @@
import leon.Utils._
-object Array4 {
+object Array5 {
def foo(a: Array[Int]): Int = {
var i = 0
diff --git a/testcases/regression/valid/Array6.scala b/testcases/regression/valid/Array6.scala
new file mode 100644
index 000000000..bdd6b0c5d
--- /dev/null
+++ b/testcases/regression/valid/Array6.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array6 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2 && a(2) == 5)
+ a(2)
+ } ensuring(_ == 5)
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
--
GitLab