diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java index 24f37cb2b90755fe5a81d0dd593a8cfe9c8a0adf..39cb3bfc1f24379ea396e1d8fc66d79de67d8432 100644 --- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java +++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java @@ -1,13 +1,7 @@ package leon.codegen.runtime; public class LeonCodeGenRuntimeException extends Exception { - private final String msg; - public LeonCodeGenRuntimeException(String msg) { - this.msg = msg; - } - - public String getMessage() { - return this.msg; + super(msg); } } diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala index de1987f5f777804ea160038391a421c6e5cddf0c..1812b0239844d2d12a3e41d71c237f69ddd2e5a9 100644 --- a/src/main/scala/leon/LeonPhase.scala +++ b/src/main/scala/leon/LeonPhase.scala @@ -2,13 +2,8 @@ package leon import purescala.Definitions.Program -abstract class LeonPhase[-F, +T] extends Pipeline[F, T] { - val name: String - val description: String - - def definedOptions: Set[LeonOptionDef] = Set() - - def run(ac: LeonContext)(v: F): T +trait LeonPhase[-F, +T] extends Pipeline[F, T] with LeonComponent { + // def run(ac: LeonContext)(v: F): T } abstract class TransformationPhase extends LeonPhase[Program, Program] { diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala index 8d455ff9b5ed73e0dd22b8e937f736e741f2ece8..12d03362a6b34ea021649f56363bf5c85791ef12 100644 --- a/src/main/scala/leon/Main.scala +++ b/src/main/scala/leon/Main.scala @@ -2,7 +2,7 @@ package leon object Main { - def allPhases: List[LeonPhase[_, _]] = { + lazy val allPhases: List[LeonPhase[_, _]] = { List( plugin.ExtractionPhase, xlang.ArrayTransformation, @@ -14,12 +14,15 @@ object Main { ) } + // Add whatever you need here. + lazy val allComponents : List[LeonComponent] = allPhases ++ Nil + lazy val allOptions = allPhases.flatMap(_.definedOptions) ++ Set( - LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis or choose() constructs"), + LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"), LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"), LeonFlagOptionDef ("parse", "--parse", "Checks only whether the program is valid PureScala"), LeonValueOptionDef("debug", "--debug=[1-5]", "Debug level"), - LeonFlagOptionDef ("help", "--help", "This help") + LeonFlagOptionDef ("help", "--help", "Show help") // Unimplemented Options: // @@ -44,15 +47,22 @@ object Main { // LeonFlagOptionDef("noLuckyTests", "--noLuckyTests", "Do not perform additional tests to potentially find models early"), // LeonFlagOptionDef("noverifymodel", "--noverifymodel", "Do not verify the correctness of models returned by Z3"), // LeonValueOptionDef("tags", "--tags=t1:...", "Filter out debug information that are not of one of the given tags"), - // LeonFlagOptionDef("oneline", "--oneline", "Reduce the output to a single line: valid if all properties were valid, invalid if at least one is invalid, unknown else") ) def displayHelp(reporter: Reporter) { reporter.info("usage: leon [--xlang] [--synthesis] [--help] [--debug=<N>] [..] <files>") reporter.info("") - reporter.info("Leon options are:") - for (opt <- allOptions.toSeq.sortBy(_.name)) { - reporter.info(" %-20s %s".format(opt.usageOption, opt.usageDesc)) + reporter.info("(By default, Leon verifies PureScala programs.)") + reporter.info("") + reporter.info("Additional options, by component:") + + for (c <- allComponents.toSeq.sortBy(_.name) if !c.definedOptions.isEmpty) { + reporter.info("") + reporter.info("%s (%s)".format(c.name, c.description)) + for(opt <- c.definedOptions.toSeq.sortBy(_.name)) { + // there is a non-breaking space at the beginning of the string :) + reporter.info("%-20s %s".format(opt.usageOption, opt.usageDesc)) + } } sys.exit(1) } diff --git a/src/main/scala/leon/plugin/ExtractorPhase.scala b/src/main/scala/leon/plugin/ExtractionPhase.scala similarity index 100% rename from src/main/scala/leon/plugin/ExtractorPhase.scala rename to src/main/scala/leon/plugin/ExtractionPhase.scala