From b67d059d8ef98ea0cb0328c176ab74b9616cd465 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 27 Oct 2014 17:12:53 +0100
Subject: [PATCH] Getting active functions, visible from main units + main
units
---
src/main/scala/leon/purescala/DefOps.scala | 6 ++++++
src/main/scala/leon/termination/TerminationChecker.scala | 3 ++-
src/main/scala/leon/termination/TerminationPhase.scala | 3 ++-
src/test/scala/leon/test/evaluators/EvaluatorsTests.scala | 6 +-----
4 files changed, 11 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 3e716313b..c374d664a 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -78,6 +78,12 @@ object DefOps {
}
}
+ def visibleFunDefsFromMain(p: Program): Set[FunDef] = {
+ p.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
+ visibleFunDefsFrom(u) ++ u.definedFunctions
+ }
+ }
+
/** Returns true for strict superpackage */
def isSuperPackageOf(p1:PackageRef, p2 : PackageRef) =
(p2.length > p1.length) &&
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index d90333484..e4273dd85 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -5,10 +5,11 @@ package termination
import purescala.Definitions._
import purescala.Trees._
+import purescala.DefOps._
abstract class TerminationChecker(val context: LeonContext, val program: Program) extends LeonComponent {
- val functions = program.definedFunctions.toSet
+ val functions = visibleFunDefsFromMain(program)
def initialize() : Unit
def terminates(funDef : FunDef) : TerminationGuarantee
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index 727f9dda4..eeba3a0ad 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -4,6 +4,7 @@ package leon
package termination
import purescala.Definitions._
+import purescala.DefOps._
object TerminationPhase extends LeonPhase[Program,TerminationReport] {
val name = "Termination"
@@ -17,7 +18,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
tc.initialize()
- val results = program.definedFunctions.toList.sortWith(_.getPos < _.getPos).map { funDef =>
+ val results = visibleFunDefsFromMain(program).toList.sortWith(_.getPos < _.getPos).map { funDef =>
(funDef -> tc.terminates(funDef))
}
val endTime = System.currentTimeMillis
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index bc203c2b8..2234f9ff3 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -38,11 +38,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
private def mkCall(name : String, args : Expr*)(implicit p : Program) = {
- p.definedFunctions.foreach { fd =>
- println(fullName(fd))
- }
-
- val fn = s"<empty>.Program.$name"
+ val fn = s"Program.$name"
searchByFullName(fn, p) match {
case Some(fd: FunDef) =>
--
GitLab