From 1288fc0b7ea52de309e2475a68631055962746be Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 13 Dec 2012 09:31:30 +0100
Subject: [PATCH] One way of handling integer command line options.
---
src/main/scala/leon/LeonOption.scala | 8 ++++++++
src/main/scala/leon/synthesis/SynthesisPhase.scala | 8 +++-----
src/main/scala/leon/verification/AnalysisPhase.scala | 10 ++++------
3 files changed, 15 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 4678772d2..1ad3cb99b 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -10,6 +10,14 @@ case class LeonFlagOption(name: String) extends LeonOption
/** Options of the form --option=value. */
case class LeonValueOption(name: String, value: String) extends LeonOption {
def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
+
+ def asInt(ctx : LeonContext) : Option[Int] = try {
+ Some(value.toInt)
+ } catch {
+ case _ : Throwable =>
+ ctx.reporter.error("Option --%s takes an integer as value.".format(name))
+ None
+ }
}
sealed abstract class LeonOptionDef {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 466abaf1d..028c7dcdd 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -47,12 +47,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case None =>
ctx.reporter.fatalError("Unknown cost model: "+cm)
}
- case LeonValueOption("timeout", t) =>
- try {
+ case v @ LeonValueOption("timeout", _) =>
+ v.asInt(ctx).foreach { t =>
options = options.copy(timeoutMs = Some(t.toLong))
- } catch {
- case _: Throwable =>
- }
+ }
case LeonFlagOption("firstonly") =>
options = options.copy(firstOnly = true)
case LeonFlagOption("parallel") =>
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index d88b73519..65e8dcce5 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -28,12 +28,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
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 v @ LeonValueOption("timeout", _) =>
+ timeout = v.asInt(ctx)
+
case _ =>
}
--
GitLab