From 543488bf1364492271728437ed3e8ac7e8b3a3f5 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 23 Jun 2015 15:57:40 +0200
Subject: [PATCH] Keep functionality of --verify --termination, and document it
---
doc/options.rst | 2 +-
src/main/scala/leon/Main.scala | 27 ++++++++++++---------------
2 files changed, 13 insertions(+), 16 deletions(-)
diff --git a/doc/options.rst b/doc/options.rst
index 140e1e56f..8d711c7a8 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -37,7 +37,7 @@ These options are mutually exclusive. By default, ``--verify`` is chosen.
* ``--termination``
- Runs a simple termination analysis.
+ Runs termination analysis. Can be used along ``--verify``.
* ``--xlang``
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 1933e5acb..8278ca339 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -37,16 +37,16 @@ object Main {
*/
object MainComponent extends LeonComponent {
val name = "main"
- val description = "Options that determine the feature of Leon to be used (mutually exclusive). Default: verify"
+ val description = "Options that select the feature of Leon to be used. Default: verify"
- val optEval = LeonStringOptionDef("eval", "Evaluate ground functions with selected evaluator", "default", "[code|default]")
+ val optEval = LeonStringOptionDef("eval", "Evaluate ground functions through code generation or evaluation (default)", "default", "[code|default]")
val optXLang = LeonFlagOptionDef("xlang", "Verification with support for extra program constructs (imperative,...)", false)
- val optTermination = LeonFlagOptionDef("termination", "Check program termination", false)
- val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
- val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
- val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
- val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", true )
- val optHelp = LeonFlagOptionDef("help", "Show help message", false)
+ val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
+ val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
+ val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
+ val optHelp = LeonFlagOptionDef("help", "Show help message", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optXLang, optNoop, optHelp, optEval, optVerify)
@@ -93,8 +93,6 @@ object Main {
val initReporter = new DefaultReporter(Set())
- val allOptions: Set[LeonOptionDef[Any]] = this.allOptions
-
val options = args.filter(_.startsWith("--")).toSet
val files = args.filterNot(_.startsWith("-")).map(new java.io.File(_))
@@ -156,14 +154,14 @@ object Main {
val repairF = ctx.findOptionOrDefault(optRepair)
val terminationF = ctx.findOptionOrDefault(optTermination)
val verifyF = ctx.findOptionOrDefault(optVerify)
- val evalF = ctx.findOption(optEval)
+ val evalF = ctx.findOption(optEval).isDefined
val analysisF = verifyF && terminationF
def debugTrees(title: String): LeonPhase[Program, Program] = {
if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
PrintTreePhase(title)
} else {
- NoopPhase[Program]
+ NoopPhase[Program]()
}
}
@@ -191,9 +189,8 @@ object Main {
else if (analysisF) Pipeline.both(FunctionClosure andThen AnalysisPhase, TerminationPhase)
else if (terminationF) TerminationPhase
else if (xlangF) XLangAnalysisPhase
- else if (evalF.isDefined) EvaluationPhase
- else if (verifyF) FunctionClosure andThen AnalysisPhase
- else NoopPhase()
+ else if (evalF) EvaluationPhase
+ else FunctionClosure andThen AnalysisPhase
}
pipeBegin andThen
--
GitLab