Getting active functions, visible from main units + main units

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) && 

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

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

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) =>