new test suite for detecting aliasing problems

src/test/resources/regression/xlang/error/ArrayAliasing1.scala

+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)
+
+}
+

src/test/resources/regression/xlang/error/ArrayAliasing2.scala

+import leon.lang._
+
+object ArrayAliasing2 {
+
+  def f1(a: Array[BigInt]): BigInt = {
+    val b = a
+    b(0) = 10
+    a(0)
+  } ensuring(_ == 10)
+
+}

src/test/resources/regression/xlang/error/ArrayAliasing3.scala

+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)
+
+}

src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala

+/* 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)
+  }
+   
+}