From 8d70434142ffd165686ae4c22ac5aaa88ce9be28 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 12 Dec 2012 19:23:44 +0100
Subject: [PATCH] timeout option back for analysis phase
---
.../leon/verification/AnalysisPhase.scala | 21 +++++++++++++++----
1 file changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index d4a2b71b7..d88b73519 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -7,7 +7,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
-import solvers.{Solver,TrivialSolver}
+import solvers.{Solver,TrivialSolver,TimeoutSolver}
import solvers.z3.FairZ3Solver
import scala.collection.mutable.{Set => MutableSet}
@@ -17,27 +17,40 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val description = "Leon Verification"
override val definedOptions : Set[LeonOptionDef] = Set(
- LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,...")
+ LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,..."),
+ LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
)
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
val functionsToAnalyse : MutableSet[String] = MutableSet.empty
+ var timeout: Option[Int] = None
for(opt <- ctx.options) opt match {
case LeonValueOption("functions", ListValue(fs)) =>
functionsToAnalyse ++= fs
+ case LeonValueOption("timeout", t) =>
+ try {
+ timeout = Some(t.toInt)
+ } catch {
+ case _: Throwable =>
+ }
case _ =>
- }
+ }
val reporter = ctx.reporter
val trivialSolver = new TrivialSolver(ctx)
val fairZ3 = new FairZ3Solver(ctx)
- val solvers : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
+ val solvers0 : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
+ val solvers: Seq[Solver] = timeout match {
+ case Some(t) => solvers0.map(s => new TimeoutSolver(s, t))
+ case None => solvers0
+ }
solvers.foreach(_.setProgram(program))
+
val defaultTactic = new DefaultTactic(reporter)
defaultTactic.setProgram(program)
val inductionTactic = new InductionTactic(reporter)
--
GitLab