From 2103d041afc8e63767e7d198a520073927053cda Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 1 Jun 2015 17:48:07 +0200
Subject: [PATCH] Termination checks library funs without @library
---
.../scala/leon/termination/TerminationPhase.scala | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index 4ad4aac3f..12af96737 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -16,7 +16,17 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
// val tc = new SimpleTerminationChecker(ctx, program)
val tc = new ComplexTerminationChecker(ctx, program)
- val results = funDefsFromMain(program).toList.sortWith(_.getPos < _.getPos).map { funDef =>
+ def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
+
+ val fdFilter = {
+ import OptionsHelpers._
+
+ filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher), Some(excludeByDefault _))
+ }
+
+ val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
+
+ val results = toVerify.map { funDef =>
funDef -> tc.terminates(funDef)
}
val endTime = System.currentTimeMillis
--
GitLab