Skip to content
Snippets Groups Projects
Commit 2103d041 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Termination checks library funs without @library

parent 053c4545
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment