diff --git a/src/test/scala/leon/test/frontends/Imports.scala b/src/test/scala/leon/test/frontends/Imports.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1475a7cd8da99f51717a901ee1b744d73cdcd778
--- /dev/null
+++ b/src/test/scala/leon/test/frontends/Imports.scala
@@ -0,0 +1,86 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.test.frontends
+
+import leon.test.LeonTestSuite
+import leon._
+import purescala.Definitions._
+import purescala.ScalaPrinter
+import frontends.scalac._
+import utils._
+
+
+class ImportsTests extends LeonTestSuite {
+ private def parseStrings(strs : List[String]) : Program = {
+ val settings : Settings = Settings(
+ verify = false,
+ injectLibrary = false
+ )
+ val reporter = new DefaultReporter(settings)
+ val context : LeonContext = LeonContext(
+ reporter,
+ new InterruptManager(reporter),
+ settings,
+ Seq()
+ )
+
+ val pipeline =
+ ExtractionPhase andThen
+ PreprocessingPhase
+
+ val inputs = strs map { str => TemporaryInputPhase.run(context)((str, Nil)).head }
+ val program = pipeline.run(testContext)(inputs)
+
+ program
+ }
+
+ // Print and reparse tests
+ private def testPrint(name : String, strs : List[String]) { test(name){
+ val orig = parseStrings(strs )
+ val output = orig.units map { ScalaPrinter(_) }
+ // If we can reparse, we consider it successful.
+ val after = parseStrings(strs)
+ }}
+
+ val testPrint1 = ("testPrint1", List(
+ """ |package foo.bar.baz
+ |import other.hello.world.Foo._
+ |
+ |object Bar {
+ | val x = 42
+ | abstract class A
+ | case class C(i : Int) extends A
+ |}
+ |
+ |object Foo {
+ | import Bar.C
+ | case class FooC()
+ | val m = Bar.x + y + x
+ | val ? = C(m)
+ | val fooC = ? match {
+ | case C(i) if i == 0 => FooC()
+ | case _ => FooC()
+ | }
+ |}""".stripMargin,
+
+ """ |package other.hello.world
+ |
+ |object Foo {
+ | val y = 0
+ |}""".stripMargin,
+
+ """ |package foo.bar
+ |package object baz {
+ | val x = 42
+ |}""".stripMargin
+ ))
+
+ for ((name,units) <- Seq(testPrint1)) {
+ testPrint(name, units)
+ }
+
+
+}
+
+
+
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ce19061f9e9b0602de72caaedacc22c522da40f6
--- /dev/null
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -0,0 +1,125 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon._
+import purescala.Definitions._
+import purescala.DefOps._
+import purescala.ScalaPrinter
+import frontends.scalac._
+import utils._
+import leon.test.LeonTestSuite
+
+private [purescala] object DefOpsHelper {
+ private def parseStrings(strs : List[String]) : Program = {
+ val settings : Settings = Settings(
+ verify = false,
+ injectLibrary = false
+ )
+ val reporter = new DefaultReporter(settings)
+ val context : LeonContext = LeonContext(
+ reporter,
+ new InterruptManager(reporter),
+ settings,
+ Seq()
+ )
+
+ val pipeline =
+ ExtractionPhase andThen
+ PreprocessingPhase
+
+ val inputs = strs map { str => TemporaryInputPhase.run(context)((str, Nil)).head }
+ val program = pipeline.run(context)(inputs)
+
+ program
+ }
+
+ val test1 = List(
+ """ |package foo.bar.baz
+ |import other.hello.world.Foo
+ |import other.hello.world.Foo._
+ |import other.hello.world.!!!._
+ |import other.hello.world.m
+ |object Bar {
+ | val x = 42
+ | abstract class A
+ | case class C(i : Int) extends A
+ |}
+ |
+ |object Foo {
+ | import Bar.C
+ | case class FooC()
+ | val m = Bar.x + y + x
+ | val ? = C(m)
+ | val fooC = ? match {
+ | case C(i) if i == 0 => FooC()
+ | case _ => FooC()
+ | }
+ |}""".stripMargin,
+
+ """ |package other.hello.world
+ |
+ |object !!! { val m = 42 }
+ |object m { val x = 0 }
+ |
+ |object Foo {
+ | val y = 0
+ |}""".stripMargin,
+
+ """ |package foo.bar
+ |package object baz {
+ | val x = 42
+ |}""".stripMargin,
+
+ """ |package foo.bar.baz.and.some.more
+ |object InSubpackage {}
+ |""".stripMargin
+ )
+ val program = parseStrings(test1)
+ val fooC = searchByFullName("foo.bar.baz.Foo.fooC",program)
+}
+
+class DefOpsTests extends LeonTestSuite {
+ import DefOpsHelper._
+
+ test("Find base definition"){assert(fooC.isDefined)}
+
+
+ test("Least common ancestor"){
+ val x = searchByFullName("foo.bar.baz.x",program)
+ assert(x.isDefined)
+ assert(leastCommonAncestor(x.get,fooC.get) == program)
+ val fooClass = searchByFullName("foo.bar.baz.Foo.FooC",program)
+ assert (fooClass.isDefined)
+ assert(leastCommonAncestor(fooC.get, fooClass.get).id.name == "Foo")
+ }
+
+ // Search by full name
+
+ def mustFind(name : String, msg : String) = test(msg) {assert(searchByFullNameRelative(name,fooC.get).isDefined) }
+ def mustFail(name : String, msg : String) = test(msg) {assert(searchByFullNameRelative(name,fooC.get).isEmpty) }
+
+ mustFind("fooC", "Find yourself")
+ mustFind("FooC", "Find a definition in the same scope 1")
+ mustFind("?", "Find a definition in the same scope 2")
+ mustFind("m", "Find a definition in the same scope 3")
+ mustFind("Foo", "Find an enclosing definition")
+ mustFind("Bar", "Find a definition in an enclosing scope")
+
+ mustFind("Bar.A", "Find a definition in an object 1")
+ mustFind("Foo.fooC", "Find a definition in an object 2")
+
+ mustFind("y", "Find imported definition 1")
+ mustFind("x", "Find imported definition 2")
+
+ mustFind("other.hello.world.Foo", "Find a definition in another package")
+ mustFind("and.some.more.InSubpackage","Find a definition in a subpackage")
+
+ mustFail("nonExistent", "Don't find non-existent definition")
+ mustFail("A", "Don't find definition in another object")
+ mustFail("InSubpackage", "Don't find definition in another package")
+ mustFail("hello.world.Foo","Don't find definition in non-visible nested package")
+ mustFail("!!!", "Don't find definition that is root of a wildcard import")
+ mustFail("m.x", "Don't find imported definition shadowed by local definition")
+
+}
\ No newline at end of file