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 0000000000000000000000000000000000000000..30b1652dac16f1f8a9c7b36d83d9a0a52811e3c6 --- /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 0000000000000000000000000000000000000000..4e906865a8848aaa00150c67de16f6b32136c64a --- /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 0000000000000000000000000000000000000000..0398fc37b9dc2028e1535878ec377bef1620dd88 --- /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 0000000000000000000000000000000000000000..41260ec2df6f9d9f32827c39e7f700da15ccca9e --- /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) + } + +}