From 25e4e292131cfe6d9bf25f9e5e88ce44f8c9d5b6 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 25 Jan 2016 17:22:55 +0100
Subject: [PATCH] disallow array equality
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 6 ++++++
.../frontends/error/simple/ArrayEquals1.scala | 10 ++++++++++
.../frontends/error/simple/ArrayEquals2.scala | 10 ++++++++++
3 files changed, 26 insertions(+)
create mode 100644 src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala
create mode 100644 src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 544947130..aa1e07e3c 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1387,6 +1387,9 @@ trait CodeExtraction extends ASTExtractors {
val rr = extractTree(r)
(rl, rr) match {
+ case (IsTyped(_, ArrayType(_)), IsTyped(_, ArrayType(_))) =>
+ outOfSubsetError(tr, "Leon does not support array comparison")
+
case (IsTyped(_, rt), IsTyped(_, lt)) if typesCompatible(lt, rt) =>
Not(Equals(rl, rr))
@@ -1405,6 +1408,9 @@ trait CodeExtraction extends ASTExtractors {
val rr = extractTree(r)
(rl, rr) match {
+ case (IsTyped(_, ArrayType(_)), IsTyped(_, ArrayType(_))) =>
+ outOfSubsetError(tr, "Leon does not support array comparison")
+
case (IsTyped(_, rt), IsTyped(_, lt)) if typesCompatible(lt, rt) =>
Equals(rl, rr)
diff --git a/src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala b/src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala
new file mode 100644
index 000000000..39a9c4b2b
--- /dev/null
+++ b/src/test/resources/regression/frontends/error/simple/ArrayEquals1.scala
@@ -0,0 +1,10 @@
+package leon.lang._
+
+object ArrayEqual1 {
+
+ def f: Boolean = {
+ Array(1,2,3) == Array(1,2,3)
+ } ensuring(res => res)
+
+}
+
diff --git a/src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala b/src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala
new file mode 100644
index 000000000..2035e0d45
--- /dev/null
+++ b/src/test/resources/regression/frontends/error/simple/ArrayEquals2.scala
@@ -0,0 +1,10 @@
+package leon.lang._
+
+object ArrayEqual2 {
+
+ def f: Boolean = {
+ Array(1,2,3) != Array(1,2,3)
+ } ensuring(res => !res)
+
+}
+
--
GitLab