From 46bf1166804259b03f119bcbc5d049e10aa25bc7 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 19 Jan 2016 16:31:37 +0100
Subject: [PATCH] support for old keyword with mutable parameters
---
.../scala/leon/xlang/AntiAliasingPhase.scala | 9 +++----
.../xlang/valid/ArrayParamMutation8.scala | 25 +++++++++++++++++++
2 files changed, 29 insertions(+), 5 deletions(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 8a5f627a7..831d5d7da 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -41,7 +41,7 @@ object AntiAliasingPhase extends TransformationPhase {
}
val res = replaceFunDefs(pgm)(fd => updatedFunctions.get(fd), (fi, fd) => None)
- println(res._1)
+ //println(res._1)
res._1
}
@@ -117,7 +117,9 @@ object AntiAliasingPhase extends TransformationPhase {
val newBody =
replace(
aliasedParams.zipWithIndex.map{ case (id, i) =>
- (id.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap +
+ (id.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap ++
+ aliasedParams.map(id =>
+ (Old(id), id.toVariable): (Expr, Expr)).toMap +
(res.toVariable -> TupleSelect(newRes.toVariable, 1)),
postBody)
Lambda(Seq(newRes), newBody).setPos(post)
@@ -272,9 +274,6 @@ object AntiAliasingPhase extends TransformationPhase {
}
def invocEffects(fi: FunctionInvocation): Set[Identifier] = {
- if(!effects.isDefinedAt(fi.tfd.fd)) {
- println("fi not defined: " + fi)
- }
//TODO: the require should be fine once we consider nested functions as well
//require(effects.isDefinedAt(fi.tfd.fd)
val mutatedParams: Set[Int] = effects.get(fi.tfd.fd).getOrElse(Set())
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala
new file mode 100644
index 000000000..68aa737eb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation8.scala
@@ -0,0 +1,25 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object ArrayParamMutation8 {
+
+ def odd(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) false
+ else {
+ a(0) = a(0) - 1
+ even(a)
+ }
+ } ensuring(res => if(old(a)(0) % 2 == 1) res else !res)
+
+ def even(a: Array[BigInt]): Boolean = {
+ require(a.length > 0 && a(0) >= 0)
+ if(a(0) == 0) true
+ else {
+ a(0) = a(0) - 1
+ odd(a)
+ }
+ } ensuring(res => if(old(a)(0) % 2 == 0) res else !res)
+
+}
--
GitLab