-
Regis Blanc authoredRegis Blanc authored
Main.scala 10.10 KiB
/* Copyright 2009-2016 EPFL, Lausanne */
package leon
import leon.utils._
object Main {
lazy val allPhases: List[LeonPhase[_, _]] = {
List(
frontends.scalac.ExtractionPhase,
frontends.scalac.ClassgenPhase,
utils.TypingPhase,
utils.FileOutputPhase,
purescala.RestoreMethods,
xlang.AntiAliasingPhase,
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
xlang.FixReportLabels,
xlang.XLangDesugaringPhase,
purescala.FunctionClosure,
synthesis.SynthesisPhase,
termination.TerminationPhase,
verification.VerificationPhase,
repair.RepairPhase,
evaluators.EvaluationPhase,
solvers.isabelle.AdaptationPhase,
solvers.isabelle.IsabellePhase,
transformations.InstrumentationPhase,
invariant.engine.InferInvariantsPhase,
laziness.LazinessEliminationPhase,
genc.GenerateCPhase,
genc.CFileOutputPhase
)
}
// Add whatever you need here.
lazy val allComponents : Set[LeonComponent] = allPhases.toSet ++ Set(
solvers.unrolling.UnrollingProcedure, MainComponent, GlobalOptions, solvers.smtlib.SMTLIBCVC4Component, solvers.isabelle.Component
)
/*
* This object holds the options that determine the selected pipeline of Leon.
* Please put any further such options here to have them print nicely in --help message.
*/
object MainComponent extends LeonComponent {
val name = "main"
val description = "Selection of Leon functionality. Default: verify"
val optEval = LeonStringOptionDef("eval", "Evaluate ground functions through code generation or evaluation (default: evaluation)", "default", "[codegen|default]")
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 optIsabelle = LeonFlagOptionDef("isabelle", "Run Isabelle verification", 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)
val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
val optLazyEval = LeonFlagOptionDef("lazy", "Handles programs that may use the 'lazy' construct", false)
val optGenc = LeonFlagOptionDef("genc", "Generate C code", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval, optGenc)
}
lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
def displayHelp(reporter: Reporter, error: Boolean) = {