diff --git a/README b/README
index 26229521988cc34cd1692b7e263ffe2316560167..4df3fcec3c92da7c14eae0260904e19bed74c362 100644
--- a/README
+++ b/README
@@ -25,13 +25,13 @@ repository and are actually automatically handled by the default build configura
To build, type this:
-xsbt clean
-xsbt package # takes a while
-xsbt script
+ $ xsbt clean
+ $ xsbt package # takes a while
+ $ xsbt script
Then you can try e.g.
-./leon testcases/sas2011-testcases/RedBlackTree.scala
+ $ ./leon ./testcases/sas2011-testcases/RedBlackTree.scala
and get something like this:
diff --git a/lib-bin/libz3.so b/lib-bin/32/libz3.so
similarity index 100%
rename from lib-bin/libz3.so
rename to lib-bin/32/libz3.so
diff --git a/lib64-bin/libz3.so b/lib-bin/64/libz3.so
similarity index 100%
rename from lib64-bin/libz3.so
rename to lib-bin/64/libz3.so
diff --git a/library/Annotations.scala b/library/src/main/scala/leon/Annotations.scala
similarity index 100%
rename from library/Annotations.scala
rename to library/src/main/scala/leon/Annotations.scala
diff --git a/library/Utils.scala b/library/src/main/scala/leon/Utils.scala
similarity index 100%
rename from library/Utils.scala
rename to library/src/main/scala/leon/Utils.scala
diff --git a/project/Build.scala b/project/Build.scala
index 1a56a0f59005de0943dd55de6ad56777bd5eb2a3..cdce363a1872dbd4a597ffc9be6e5f2be44868f5 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -6,75 +6,86 @@ object Leon extends Build {
private val scriptName = "leon"
def scriptFile = file(".") / scriptName
def is64 = System.getProperty("sun.arch.data.model") == "64"
- def ldLibraryDir32 = file(".") / "lib-bin"
- def ldLibraryDir64 = file(".") / "lib64-bin"
+ def ldLibraryDir32 = file(".") / "lib-bin" / "32"
+ def ldLibraryDir64 = file(".") / "lib-bin" / "64"
+
+ val cleanTask = TaskKey[Unit]("clean", "Cleans up the generated binaries and scripts.") <<= (streams, clean) map { (s,c) =>
+ c
+ if(scriptFile.exists && scriptFile.isFile) {
+ scriptFile.delete
+ }
+ }
val scriptTask = TaskKey[Unit]("script", "Generate the " + scriptName + " Bash script") <<= (streams, dependencyClasspath in Compile, classDirectory in Compile) map { (s, deps, out) =>
- if(!scriptFile.exists) {
+ if(scriptFile.exists) {
+ s.log.info("Re-generating script ("+(if(is64) "64b" else "32b")+")...")
+ scriptFile.delete
+ } else {
s.log.info("Generating script ("+(if(is64) "64b" else "32b")+")...")
- try {
- val depsPaths = deps.map(_.data.absolutePath)
-
- val depsPaths64 = depsPaths.filterNot(_.endsWith("unmanaged/z3.jar"))
- val depsPaths32 = depsPaths.filterNot(_.endsWith("unmanaged/z3-64.jar"))
-
- // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
- val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
- case None => throw new Exception("Couldn't guess SCALA_HOME.")
- case Some(p) => p.substring(0, p.length - 21)
- }
- s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
-
- val nl = System.getProperty("line.separator")
- val fw = new java.io.FileWriter(scriptFile)
- fw.write("#!/bin/bash --posix" + nl)
- if (is64) {
+ }
+ try {
+ val depsPaths = deps.map(_.data.absolutePath)
+
+ val depsPaths64 = depsPaths.filterNot(_.endsWith("unmanaged/z3.jar"))
+ val depsPaths32 = depsPaths.filterNot(_.endsWith("unmanaged/z3-64.jar"))
+
+ // One ugly hack... Likely to fail for Windows, but it's a Bash script anyway.
+ val scalaHomeDir = depsPaths.find(_.endsWith("lib/scala-library.jar")) match {
+ case None => throw new Exception("Couldn't guess SCALA_HOME.")
+ case Some(p) => p.substring(0, p.length - 21)
+ }
+ s.log.info("Will use " + scalaHomeDir + " as SCALA_HOME.")
+
+ val nl = System.getProperty("line.separator")
+ val fw = new java.io.FileWriter(scriptFile)
+ fw.write("#!/bin/bash --posix" + nl)
+ if (is64) {
+ fw.write("SCALACLASSPATH=\"")
+ fw.write((out.absolutePath +: depsPaths64).mkString(":"))
+ fw.write("\"" + nl + nl)
+
+ // Setting the dynamic lib path
+ fw.write("LIBRARY_PATH=\"" + ldLibraryDir64.absolutePath + "\"" + nl)
+ } else {
+ fw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
+
fw.write("SCALACLASSPATH=\"")
fw.write((out.absolutePath +: depsPaths64).mkString(":"))
fw.write("\"" + nl + nl)
// Setting the dynamic lib path
fw.write("LIBRARY_PATH=\"" + ldLibraryDir64.absolutePath + "\"" + nl)
- } else {
- fw.write("if [ `uname -m` == \"x86_64\" ]; then "+nl)
-
- fw.write("SCALACLASSPATH=\"")
- fw.write((out.absolutePath +: depsPaths64).mkString(":"))
- fw.write("\"" + nl + nl)
-
- // Setting the dynamic lib path
- fw.write("LIBRARY_PATH=\"" + ldLibraryDir64.absolutePath + "\"" + nl)
-
- fw.write("else" + nl)
-
- fw.write("SCALACLASSPATH=\"")
- fw.write((out.absolutePath +: depsPaths32).mkString(":"))
- fw.write("\"" + nl + nl)
-
- // Setting the dynamic lib path
- fw.write("LIBRARY_PATH=\"" + ldLibraryDir32.absolutePath + "\"" + nl)
- fw.write("fi" + nl)
-
- }
-
- // the Java command that uses sbt's local Scala to run the whole contraption.
- fw.write("LD_LIBRARY_PATH=\"$LIBRARY_PATH\" \\"+nl)
- fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"")
- fw.write(scalaHomeDir)
- fw.write("\" -Dscala.usejavacp=true ")
- fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
- fw.write("leon.Main $@" + nl)
- fw.close
- scriptFile.setExecutable(true)
- } catch {
- case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
+
+ fw.write("else" + nl)
+
+ fw.write("SCALACLASSPATH=\"")
+ fw.write((out.absolutePath +: depsPaths32).mkString(":"))
+ fw.write("\"" + nl + nl)
+
+ // Setting the dynamic lib path
+ fw.write("LIBRARY_PATH=\"" + ldLibraryDir32.absolutePath + "\"" + nl)
+ fw.write("fi" + nl)
+
}
+
+ // the Java command that uses sbt's local Scala to run the whole contraption.
+ fw.write("LD_LIBRARY_PATH=\"$LIBRARY_PATH\" \\"+nl)
+ fw.write("java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.home=\"")
+ fw.write(scalaHomeDir)
+ fw.write("\" -Dscala.usejavacp=true ")
+ fw.write("scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} ")
+ fw.write("leon.Main $@" + nl)
+ fw.close
+ scriptFile.setExecutable(true)
+ } catch {
+ case e => s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
}
}
object LeonProject {
val settings = Seq(
- scriptTask
+ scriptTask,
+ cleanTask
)
}