Skip to content
Snippets Groups Projects
Commit 6b811a32 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Always include lib

parent 2540be11
No related branches found
No related tags found
No related merge requests found
...@@ -34,7 +34,6 @@ object Main { ...@@ -34,7 +34,6 @@ object Main {
LeonFlagOptionDef ("termination", "--termination", "Check program termination"), LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"), LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"), LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonFlagOptionDef ("library", "--library", "Inject Leon standard library"),
LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt)"), LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt)"),
LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"), LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"),
LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"), LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"),
...@@ -143,8 +142,6 @@ object Main { ...@@ -143,8 +142,6 @@ object Main {
settings = settings.copy(termination = value) settings = settings.copy(termination = value)
case LeonFlagOption("synthesis", value) => case LeonFlagOption("synthesis", value) =>
settings = settings.copy(synthesis = value) settings = settings.copy(synthesis = value)
case LeonFlagOption("library", value) =>
settings = settings.copy(injectLibrary = value)
case LeonFlagOption("xlang", value) => case LeonFlagOption("xlang", value) =>
settings = settings.copy(xlang = value) settings = settings.copy(xlang = value)
case LeonValueOption("solvers", ListValue(ss)) => case LeonValueOption("solvers", ListValue(ss)) =>
...@@ -231,19 +228,12 @@ object Main { ...@@ -231,19 +228,12 @@ object Main {
pipeProcess pipeProcess
} }
def main(args : Array[String]) { def main(args: Array[String]) {
val argsl = args.toList val argsl = args.toList
// By default we add --library from Main
val realArgs = if (!args.exists(_.contains("--library"))) {
"--library" :: argsl
} else {
argsl
}
// Process options // Process options
val ctx = try { val ctx = try {
processOptions(realArgs) processOptions(argsl)
} catch { } catch {
case LeonFatalError(None) => case LeonFatalError(None) =>
sys.exit(1) sys.exit(1)
......
...@@ -11,6 +11,5 @@ case class Settings( ...@@ -11,6 +11,5 @@ case class Settings(
val synthesis: Boolean = false, val synthesis: Boolean = false,
val xlang: Boolean = false, val xlang: Boolean = false,
val verify: Boolean = true, val verify: Boolean = true,
val injectLibrary: Boolean = false,
val selectedSolvers: Set[String] = Set("fairz3") val selectedSolvers: Set[String] = Set("fairz3")
) )
...@@ -35,15 +35,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] { ...@@ -35,15 +35,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
settings.Yrangepos.value = true settings.Yrangepos.value = true
settings.skip.value = List("patmat") settings.skip.value = List("patmat")
val libFiles = Build.libFiles val compilerOpts = Build.libFiles ::: args.filterNot(_.startsWith("--"))
val injected = if (ctx.settings.injectLibrary) {
libFiles
} else {
libFiles.filter(f => (f.contains("/lang/") && !f.contains("/lang/string/")) || f.contains("/annotation/"))
}
val compilerOpts = injected ::: args.filterNot(_.startsWith("--"))
val command = new CompilerCommand(compilerOpts, settings) { val command = new CompilerCommand(compilerOpts, settings) {
override val cmdName = "leon" override val cmdName = "leon"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment