From 205a5caaecf698783011cee250085147a5532281 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 7 Mar 2012 14:54:42 +0100
Subject: [PATCH] Moved Main.scala outside of plugin package and show help when
invalid option is provided.
---
project/Build.scala | 2 +-
src/main/scala/leon/{plugin => }/Main.scala | 11 +++--
src/main/scala/leon/plugin/LeonPlugin.scala | 46 ++++++++++-----------
3 files changed, 29 insertions(+), 30 deletions(-)
rename src/main/scala/leon/{plugin => }/Main.scala (83%)
diff --git a/project/Build.scala b/project/Build.scala
index 591ae1131..c96f110f2 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -34,7 +34,7 @@ object Leon extends Build {
fw.write(scalaHomeDir)
fw.write("\" -Dscala.usejavacp=true ")
fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
- fw.write("leon.plugin.Main $@" + nl)
+ fw.write("leon.Main $@" + nl)
fw.close
scriptFile.setExecutable(true)
} catch {
diff --git a/src/main/scala/leon/plugin/Main.scala b/src/main/scala/leon/Main.scala
similarity index 83%
rename from src/main/scala/leon/plugin/Main.scala
rename to src/main/scala/leon/Main.scala
index 027b35a70..aefcf528a 100644
--- a/src/main/scala/leon/plugin/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -1,7 +1,6 @@
package leon
-package plugin
-import scala.tools.nsc.{Global,Settings,SubComponent,CompilerCommand}
+import scala.tools.nsc.{Global,Settings=>NSCSettings,SubComponent,CompilerCommand}
import purescala.Definitions.Program
@@ -26,7 +25,7 @@ object Main {
}
def run(args: Array[String], reporter: Reporter = new DefaultReporter, classPath : Option[Seq[String]] = None) : Unit = {
- val settings = new Settings
+ val settings = new NSCSettings
classPath.foreach(s => settings.classpath.tryToSet(s.toList))
runWithSettings(args, settings, s => reporter.info(s), Some(p => defaultAction(p, reporter)))
}
@@ -36,7 +35,7 @@ object Main {
analysis.analyse
}
- private def runWithSettings(args : Array[String], settings : Settings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
+ private def runWithSettings(args : Array[String], settings : NSCSettings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
val (leonOptions, nonLeonOptions) = args.toList.partition(_.startsWith("--"))
val command = new CompilerCommand(nonLeonOptions, settings) {
override val cmdName = "leon"
@@ -58,8 +57,8 @@ object Main {
/** This class is a compiler that will be used for running the plugin in
* standalone mode. Original version courtesy of D. Zufferey. */
-class PluginRunner(settings : Settings, reportingFunction : String => Unit, actionOnProgram : Option[Program=>Unit]) extends Global(settings, new SimpleReporter(settings, reportingFunction)) {
- val leonPlugin = new LeonPlugin(this, actionOnProgram)
+class PluginRunner(settings : NSCSettings, reportingFunction : String => Unit, actionOnProgram : Option[Program=>Unit]) extends Global(settings, new plugin.SimpleReporter(settings, reportingFunction)) {
+ val leonPlugin = new plugin.LeonPlugin(this, actionOnProgram)
protected def myAddToPhasesSet(sub : SubComponent, descr : String) : Unit = {
phasesSet += sub
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 39356927d..fbbf2b834 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -19,28 +19,28 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
/** The help message displaying the options for that plugin. */
override val optionsHelp: Option[String] = Some(
- " -P:leon:uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
- " -P:leon:with-code Allows the compiler to keep running after the static analysis" + "\n" +
- " -P:leon:parse Checks only whether the program is valid PureScala" + "\n" +
- " -P:leon:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
- " -P:leon:nodefaults Runs only the analyses provided by the extensions" + "\n" +
- " -P:leon:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
- " -P:leon:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
- " -P:leon:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
- " -P:leon:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
- " -P:leon:bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
- " -P:leon:impure Generate testcases only for impure functions" + "\n" +
- " -P:leon:testcases=[1,2] Number of testcases to generate per function" + "\n" +
- " -P:leon:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
- " -P:leon:timeout=N Sets a timeout of N seconds" + "\n" +
- " -P:leon:XP Enable weird transformations and other bug-producing features" + "\n" +
- " -P:leon:BV Use bit-vectors for integers" + "\n" +
- " -P:leon:prune Use additional SMT queries to rule out some unrollings" + "\n" +
- " -P:leon:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
- " -P:leon:quickcheck Use QuickCheck-like random search" + "\n" +
- " -P:leon:parallel Run all solvers in parallel" + "\n" +
- " -P:leon:templates Use new ``FunctionTemplate'' technique" + "\n" +
- " -P:leon:noLuckyTests Do not perform additional tests to potentially find models early"
+ " --uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
+ " --with-code Allows the compiler to keep running after the static analysis" + "\n" +
+ " --parse Checks only whether the program is valid PureScala" + "\n" +
+ " --extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
+ " --nodefaults Runs only the analyses provided by the extensions" + "\n" +
+ " --functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
+ " --unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
+ " --axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
+ " --tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
+ " --bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
+ " --impure Generate testcases only for impure functions" + "\n" +
+ " --testcases=[1,2] Number of testcases to generate per function" + "\n" +
+ " --testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
+ " --timeout=N Sets a timeout of N seconds" + "\n" +
+ " --XP Enable weird transformations and other bug-producing features" + "\n" +
+ " --BV Use bit-vectors for integers" + "\n" +
+ " --prune Use additional SMT queries to rule out some unrollings" + "\n" +
+ " --cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
+ " --quickcheck Use QuickCheck-like random search" + "\n" +
+ " --parallel Run all solvers in parallel" + "\n" +
+ " --templates Use new ``FunctionTemplate'' technique" + "\n" +
+ " --noLuckyTests Do not perform additional tests to potentially find models early"
)
/** Processes the command-line options. */
@@ -70,7 +70,7 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
case s if s.startsWith("testbounds=") => leon.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
case s if s.startsWith("timeout=") => leon.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
case s if s.startsWith("testcases=") => leon.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
- case _ => error("Invalid option: " + option)
+ case _ => error("Invalid option: " + option + "\nValid options are:\n" + optionsHelp.get)
}
}
}
--
GitLab