From 69b8aa703e2a767f6665cb6a5d6fb774f132f8e7 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 14 Jan 2016 15:36:45 +0100
Subject: [PATCH] new test suite for detecting aliasing problems
---
.../xlang/error/ArrayAliasing1.scala | 13 ++++++
.../xlang/error/ArrayAliasing2.scala | 11 +++++
.../xlang/error/ArrayAliasing3.scala | 11 +++++
.../xlang/XLangDesugaringSuite.scala | 46 +++++++++++++++++++
4 files changed, 81 insertions(+)
create mode 100644 src/test/resources/regression/xlang/error/ArrayAliasing1.scala
create mode 100644 src/test/resources/regression/xlang/error/ArrayAliasing2.scala
create mode 100644 src/test/resources/regression/xlang/error/ArrayAliasing3.scala
create mode 100644 src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing1.scala b/src/test/resources/regression/xlang/error/ArrayAliasing1.scala
new file mode 100644
index 000000000..30b1652da
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing1.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object ArrayAliasing1 {
+
+ def f1(): BigInt = {
+ val a = Array.fill(10)(BigInt(0))
+ val b = a
+ b(0) = 10
+ a(0)
+ } ensuring(_ == 10)
+
+}
+
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing2.scala b/src/test/resources/regression/xlang/error/ArrayAliasing2.scala
new file mode 100644
index 000000000..4e906865a
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing2.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing2 {
+
+ def f1(a: Array[BigInt]): BigInt = {
+ val b = a
+ b(0) = 10
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing3.scala b/src/test/resources/regression/xlang/error/ArrayAliasing3.scala
new file mode 100644
index 000000000..0398fc37b
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing3.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+
+object ArrayAliasing3 {
+
+ def f1(a: Array[BigInt], b: Boolean): BigInt = {
+ val c = if(b) a else Array[BigInt](1,2,3,4,5)
+ c(0) = 10
+ a(0)
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
new file mode 100644
index 000000000..41260ec2d
--- /dev/null
+++ b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
@@ -0,0 +1,46 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.regression.xlang
+
+import leon._
+import leon.test._
+import purescala.Definitions.Program
+import java.io.File
+
+class XLangDesugaringSuite extends LeonRegressionSuite {
+ // Hard-code output directory, for Eclipse purposes
+
+ val pipeline = frontends.scalac.ExtractionPhase andThen new utils.PreprocessingPhase(true)
+
+ def testFrontend(f: File, forError: Boolean) = {
+ test ("Testing " + f.getName) {
+ val ctx = createLeonContext()
+ if (forError) {
+ intercept[LeonFatalError]{
+ pipeline.run(ctx, List(f.getAbsolutePath))
+ }
+ } else {
+ pipeline.run(ctx, List(f.getAbsolutePath))
+ }
+ }
+
+ }
+
+ private def forEachFileIn(path : String)(block : File => Unit) {
+ val fs = filesInResourceDir(path, _.endsWith(".scala"))
+
+ for(f <- fs) {
+ block(f)
+ }
+ }
+
+ val baseDir = "regression/xlang/"
+
+ forEachFileIn(baseDir+"passing/") { f =>
+ testFrontend(f, false)
+ }
+ forEachFileIn(baseDir+"error/") { f =>
+ testFrontend(f, true)
+ }
+
+}
--
GitLab