From fcd94c478f2ad899bd0668224a7a289accec1d29 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 24 Oct 2014 10:17:19 +0100
Subject: [PATCH] Treat <empty> package
---
.../leon/frontends/scalac/CodeExtraction.scala | 6 +++++-
.../scala/leon/test/purescala/DefOpsTests.scala | 14 ++++++++++++--
2 files changed, 17 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3f96d9488..40e3a6117 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -327,7 +327,11 @@ trait CodeExtraction extends ASTExtractors {
}
private def extractPackageRef(refPath : RefTree) : PackageRef =
- getSelectChain(refPath.qualifier) :+ refPath.name.toString
+ (getSelectChain(refPath.qualifier) :+ refPath.name.toString) match {
+ // Make sure to drop "<empty>" package
+ case List("<empty>") => List()
+ case other => other
+ }
private def extractImport(i : Import, current : UnitDef, units : List[UnitDef]) : Seq[ LeonImport ] = i match { case Import(expr, sels) =>
import DefOps._
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
index 605e5012b..f6a062f16 100644
--- a/src/test/scala/leon/test/purescala/DefOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -72,7 +72,9 @@ private [purescala] object DefOpsHelper {
""" |package foo.bar.baz.and.some.more
|object InSubpackage {}
- |""".stripMargin
+ |""".stripMargin,
+
+ """ object InEmpty { def arrayLookup(a : Array[Int], i : Int) = a(i) } """
)
val program = parseStrings(test1)
val fooC = searchByFullName("foo.bar.baz.Foo.fooC",program)
@@ -91,6 +93,13 @@ class DefOpsTests extends LeonTestSuite {
val fooClass = searchByFullName("foo.bar.baz.Foo.FooC",program)
assert (fooClass.isDefined)
assert(leastCommonAncestor(fooC.get, fooClass.get).id.name == "Foo")
+ }
+
+ test("In empty package") {
+ val name = "InEmpty.arrayLookup"
+ val df = searchByFullName(name,program)
+ assert(df.isDefined)
+ assert{fullName(df.get) == name }
}
// Search by full name
@@ -113,7 +122,8 @@ class DefOpsTests extends LeonTestSuite {
mustFind("other.hello.world.Foo", "Find a definition in another package")
mustFind("and.some.more.InSubpackage","Find a definition in a subpackage")
-
+ mustFind("InEmpty.arrayLookup", "Find a definition in the empty package")
+
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")
--
GitLab