diff --git a/src/main/scala/leon/codegen/CodeGen.scala b/src/main/scala/leon/codegen/CodeGen.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7f84a897682d716f751f12dbdb68cdf00f9466de
--- /dev/null
+++ b/src/main/scala/leon/codegen/CodeGen.scala
@@ -0,0 +1,14 @@
+package leon
+package codegen
+
+import purescala.Common._
+import purescala.Definitions._
+
+object CodeGenPhase extends LeonPhase[Program,CompilationResult] {
+ val name = "CodeGen"
+ val description = "Compiles a Leon program into Java methods"
+
+ def run(ctx : LeonContext)(p : Program) : CompilationResult = {
+ CompilationResult(successful = true)
+ }
+}
diff --git a/src/main/scala/leon/codegen/CompilationResult.scala b/src/main/scala/leon/codegen/CompilationResult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dbb267c3c236c4c31f2dc10d50f1ed9ab4861301
--- /dev/null
+++ b/src/main/scala/leon/codegen/CompilationResult.scala
@@ -0,0 +1,6 @@
+package leon
+package codegen
+
+case class CompilationResult(
+ successful : Boolean = false
+)
diff --git a/src/test/resources/regression/codegen/purescala/Prog001.scala b/src/test/resources/regression/codegen/purescala/Prog001.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c0eb52647720910e8f9a43c19a3af4f88c10261b
--- /dev/null
+++ b/src/test/resources/regression/codegen/purescala/Prog001.scala
@@ -0,0 +1,3 @@
+object Prog001 {
+ def plus(x : Int, y : Int) : Int = x + y
+}
diff --git a/src/test/resources/regression/codegen/purescala/README b/src/test/resources/regression/codegen/purescala/README
new file mode 100644
index 0000000000000000000000000000000000000000..2edec540798afef79cf99eae4253420d89fbc890
--- /dev/null
+++ b/src/test/resources/regression/codegen/purescala/README
@@ -0,0 +1,2 @@
+This directory contains PureScala programs for which compilation (codegen)
+should always succeed entirely.
diff --git a/src/test/scala/leon/test/Test.scala b/src/test/scala/leon/test/Test.scala
deleted file mode 100644
index ed3549395b971f0e12fbdb8a8c7656526fe936e8..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/Test.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-package leon.test
-
-import org.scalatest.FunSuite
-
-class Test extends FunSuite {
- test("Tests work.") {
- assert(true)
- }
-}
diff --git a/src/test/scala/leon/test/TestUtils.scala b/src/test/scala/leon/test/TestUtils.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0177d25dc362236a913cc261d3366f9e6750962e
--- /dev/null
+++ b/src/test/scala/leon/test/TestUtils.scala
@@ -0,0 +1,22 @@
+package leon
+package test
+
+import java.io.File
+
+object TestUtils {
+ private val all : String=>Boolean = (s : String) => true
+
+ def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = {
+ import scala.collection.JavaConversions._
+
+ val d = this.getClass.getClassLoader.getResource(dir)
+
+ if(d == null || d.getProtocol != "file") {
+ assert(false, "Tests have to be run from within `sbt`, for otherwise the test files will be harder to access (and we dislike that).")
+ }
+
+ val asFile = new File(d.toURI())
+
+ asFile.listFiles().filter(f => filter(f.getPath()))
+ }
+}
diff --git a/src/test/scala/leon/test/codegen/CodeGenRegression.scala b/src/test/scala/leon/test/codegen/CodeGenRegression.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2c15669473e00ce074c8ab0f010a6f38b957e0c
--- /dev/null
+++ b/src/test/scala/leon/test/codegen/CodeGenRegression.scala
@@ -0,0 +1,73 @@
+package leon.test
+package codegen
+
+import leon._
+import leon.plugin.ExtractionPhase
+import leon.codegen.CodeGenPhase
+import leon.codegen.CompilationResult
+
+import org.scalatest.FunSuite
+
+import java.io.File
+
+import TestUtils._
+
+class CodeGenRegression extends FunSuite {
+ private var counter : Int = 0
+ private def nextInt() : Int = {
+ counter += 1
+ counter
+ }
+
+ private case class Output(result : CompilationResult, reporter : Reporter)
+
+ private def mkPipeline : Pipeline[List[String],CompilationResult] =
+ ExtractionPhase andThen CodeGenPhase
+
+ private def mkTest(file : File)(block: Output=>Unit) = {
+ val fullName = file.getPath()
+ val start = fullName.indexOf("regression")
+ val displayName = if(start != -1) {
+ fullName.substring(start, fullName.length)
+ } else {
+ fullName
+ }
+
+ test("PureScala program %3d: [%s]".format(nextInt(), displayName)) {
+ assert(file.exists && file.isFile && file.canRead,
+ "Benchmark [%s] is not a readable file".format(displayName))
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = false,
+ xlang = false,
+ verify = false
+ ),
+ files = List(file),
+ reporter = new SilentReporter
+ )
+
+ val pipeline = mkPipeline
+
+ val result = pipeline.run(ctx)(file.getPath :: Nil)
+
+ block(Output(result, ctx.reporter))
+ }
+ }
+
+ private def forEachFileIn(cat : String)(block : Output=>Unit) {
+ val fs = filesInResourceDir(
+ "regression/codegen/" + cat,
+ _.endsWith(".scala"))
+
+ for(f <- fs) {
+ mkTest(f)(block)
+ }
+ }
+
+ forEachFileIn("purescala") { output =>
+ val Output(result, reporter) = output
+ assert(result.successful, "Compilation should be successful.")
+ assert(reporter.errorCount === 0)
+ assert(reporter.warningCount === 0)
+ }
+}
diff --git a/src/test/scala/leon/test/PureScalaPrograms.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
similarity index 74%
rename from src/test/scala/leon/test/PureScalaPrograms.scala
rename to src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index ff95fa366d9c93b9ccbf691cfb097af5a375f115..0a615a3e9d5dfdb31a4e74b22163850930cc81a4 100644
--- a/src/test/scala/leon/test/PureScalaPrograms.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -1,5 +1,6 @@
package leon
package test
+package verification
import leon.verification.{AnalysisPhase,VerificationReport}
@@ -7,7 +8,9 @@ import org.scalatest.FunSuite
import java.io.File
-class PureScalaPrograms extends FunSuite {
+import TestUtils._
+
+class PureScalaVerificationRegression extends FunSuite {
private var counter : Int = 0
private def nextInt() : Int = {
counter += 1
@@ -50,22 +53,17 @@ class PureScalaPrograms extends FunSuite {
}
}
- private def forEachFileIn(dirName : String)(block : Output=>Unit) {
- import scala.collection.JavaConversions._
-
- val dir = this.getClass.getClassLoader.getResource(dirName)
-
- if(dir == null || dir.getProtocol != "file") {
- assert(false, "Tests have to be run from within `sbt`, for otherwise " +
- "the test files will be harder to access (and we dislike that).")
- }
+ private def forEachFileIn(cat : String)(block : Output=>Unit) {
+ val fs = filesInResourceDir(
+ "regression/verification/purescala/" + cat,
+ _.endsWith(".scala"))
- for(f <- (new File(dir.toURI())).listFiles() if f.getPath().endsWith(".scala")) {
+ for(f <- fs) {
mkTest(f)(block)
}
}
- forEachFileIn("regression/verification/purescala/valid") { output =>
+ forEachFileIn("valid") { output =>
val Output(report, reporter) = output
assert(report.totalConditions === report.totalValid,
"All verification conditions ("+report.totalConditions+") should be valid.")
@@ -73,7 +71,7 @@ class PureScalaPrograms extends FunSuite {
assert(reporter.warningCount === 0)
}
- forEachFileIn("regression/verification/purescala/invalid") { output =>
+ forEachFileIn("invalid") { output =>
val Output(report, reporter) = output
assert(report.totalInvalid > 0,
"There should be at least one invalid verification condition.")
diff --git a/unmanaged/32/cafebabe_2.9.2-1.2.jar b/unmanaged/32/cafebabe_2.9.2-1.2.jar
new file mode 100644
index 0000000000000000000000000000000000000000..57defc82adbd3db0baa2f7bfe33f08f1ee2f9e38
Binary files /dev/null and b/unmanaged/32/cafebabe_2.9.2-1.2.jar differ