From c85e1da24f7a2e3669d4c9509b9f6895e3f37934 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 6 Apr 2016 22:37:31 +0200
Subject: [PATCH] fix excessive renaming in xlang
---
.../scala/leon/xlang/AntiAliasingPhase.scala | 5 ++++-
.../HigherOrderFunctionsMutableParams7.scala | 19 +++++++++++++++++++
2 files changed, 23 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 3b80989e6..fadab3b73 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -77,7 +77,10 @@ object AntiAliasingPhase extends TransformationPhase {
}.map(_.id)
val newParams = fd.params.map(vd => vd.getType match {
- case (ft: FunctionType) => ValDef(vd.id.duplicate(tpe = makeFunctionTypeExplicit(ft)))
+ case (ft: FunctionType) => {
+ val nft = makeFunctionTypeExplicit(ft)
+ if(ft == nft) vd else ValDef(vd.id.duplicate(tpe = nft))
+ }
case _ => vd
})
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala
new file mode 100644
index 000000000..b32043f00
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala
@@ -0,0 +1,19 @@
+object HigherOrderFunctionsMutableParams7 {
+ /*
+ * this test catches an error that happened in
+ * xlang when renaming higher order functions parameter
+ * even though the function had a pure signature (Int => Int)
+ */
+
+ def app(f: (Int) => Int, x: Int): Int = {
+ f(x)
+ }
+
+ def id(x: Int) = x
+
+ def test(): Int = {
+ val x = 12
+ app(id, 12)
+ } ensuring(_ == 12)
+
+}
--
GitLab