From 6b811a321e5ed137d9c9ac19bbae9d7377327e55 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 23 Oct 2014 16:23:26 +0200
Subject: [PATCH] Always include lib
---
src/main/scala/leon/Main.scala | 14 ++------------
src/main/scala/leon/Settings.scala | 1 -
.../leon/frontends/scalac/ExtractionPhase.scala | 10 +---------
3 files changed, 3 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b51a0746b..22fa23f61 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -34,7 +34,6 @@ object Main {
LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
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("debug", "--debug=<sections..>", "Enables specific messages"),
LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"),
@@ -143,8 +142,6 @@ object Main {
settings = settings.copy(termination = value)
case LeonFlagOption("synthesis", value) =>
settings = settings.copy(synthesis = value)
- case LeonFlagOption("library", value) =>
- settings = settings.copy(injectLibrary = value)
case LeonFlagOption("xlang", value) =>
settings = settings.copy(xlang = value)
case LeonValueOption("solvers", ListValue(ss)) =>
@@ -231,19 +228,12 @@ object Main {
pipeProcess
}
- def main(args : Array[String]) {
+ def main(args: Array[String]) {
val argsl = args.toList
- // By default we add --library from Main
- val realArgs = if (!args.exists(_.contains("--library"))) {
- "--library" :: argsl
- } else {
- argsl
- }
-
// Process options
val ctx = try {
- processOptions(realArgs)
+ processOptions(argsl)
} catch {
case LeonFatalError(None) =>
sys.exit(1)
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 52ede3a61..4ad409af2 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -11,6 +11,5 @@ case class Settings(
val synthesis: Boolean = false,
val xlang: Boolean = false,
val verify: Boolean = true,
- val injectLibrary: Boolean = false,
val selectedSolvers: Set[String] = Set("fairz3")
)
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 7ab531088..970c82ca0 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -35,15 +35,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
settings.Yrangepos.value = true
settings.skip.value = List("patmat")
- val libFiles = Build.libFiles
-
- 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 compilerOpts = Build.libFiles ::: args.filterNot(_.startsWith("--"))
val command = new CompilerCommand(compilerOpts, settings) {
override val cmdName = "leon"
--
GitLab