diff --git a/src/main/scala/funcheck/FunCheckPlugin.scala b/src/main/scala/funcheck/FunCheckPlugin.scala
deleted file mode 100644
index 8799f320fad7f16eb89581d1d82abeddb89773b7..0000000000000000000000000000000000000000
--- a/src/main/scala/funcheck/FunCheckPlugin.scala
+++ /dev/null
@@ -1,79 +0,0 @@
-package funcheck
-
-import scala.tools.nsc
-import scala.tools.nsc.{Global,Phase}
-import scala.tools.nsc.plugins.{Plugin,PluginComponent}
-import purescala.Definitions.Program
-
-/** This class is the entry point for the plugin. */
-class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Program=>Unit] = None) extends Plugin {
- import global._
-
- val name = "funcheck"
- val description = "Static analysis for Scala by LARA."
-
- var stopAfterAnalysis: Boolean = true
- var stopAfterExtraction: Boolean = false
- var silentlyTolerateNonPureBodies: Boolean = false
-
- /** The help message displaying the options for that plugin. */
- override val optionsHelp: Option[String] = Some(
- " -P:funcheck:uniqid When pretty-printing funcheck trees, show identifiers IDs" + "\n" +
- " -P:funcheck:with-code Allows the compiler to keep running after the static analysis" + "\n" +
- " -P:funcheck:parse Checks only whether the program is valid PureScala" + "\n" +
- " -P:funcheck:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
- " -P:funcheck:nodefaults Runs only the analyses provided by the extensions" + "\n" +
- " -P:funcheck:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
- " -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
- " -P:funcheck:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
- " -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
- " -P:funcheck:bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
- " -P:funcheck:impure Generate testcases only for impure functions" + "\n" +
- " -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" +
- " -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
- " -P:funcheck:timeout=N Sets a timeout of N seconds" + "\n" +
- " -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
- " -P:funcheck:BV Use bit-vectors for integers" + "\n" +
- " -P:funcheck:prune Use additional SMT queries to rule out some unrollings" + "\n" +
- " -P:funcheck:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
- " -P:funcheck:quickcheck Use QuickCheck-like random search" + "\n" +
- " -P:funcheck:parallel Run all solvers in parallel" + "\n" +
- " -P:funcheck:templates Use new ``FunctionTemplate'' technique" + "\n" +
- " -P:funcheck:noLuckyTests Do not perform additional tests to potentially find models early"
- )
-
- /** Processes the command-line options. */
- private def splitList(lst: String) : Seq[String] = lst.split(':').map(_.trim).filter(!_.isEmpty)
- override def processOptions(options: List[String], error: String => Unit) {
- for(option <- options) {
- option match {
- case "with-code" => stopAfterAnalysis = false
- case "uniqid" => purescala.Settings.showIDs = true
- case "parse" => stopAfterExtraction = true
- case "tolerant" => silentlyTolerateNonPureBodies = true
- case "nodefaults" => purescala.Settings.runDefaultExtensions = false
- case "axioms" => purescala.Settings.noForallAxioms = false
- case "bapa" => purescala.Settings.useBAPA = true
- case "impure" => purescala.Settings.impureTestcases = true
- case "XP" => purescala.Settings.experimental = true
- case "BV" => purescala.Settings.bitvectorBitwidth = Some(32)
- case "prune" => purescala.Settings.pruneBranches = true
- case "cores" => purescala.Settings.useCores = true
- case "quickcheck" => purescala.Settings.useQuickCheck = true
- case "parallel" => purescala.Settings.useParallel = true
- case "templates" => purescala.Settings.useTemplates = true
- case "noLuckyTests" => purescala.Settings.luckyTest = false
- case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
- case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
- case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
- case s if s.startsWith("testbounds=") => purescala.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
- case s if s.startsWith("timeout=") => purescala.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
- case s if s.startsWith("testcases=") => purescala.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
- case _ => error("Invalid option: " + option)
- }
- }
- }
-
- val components = List[PluginComponent](new AnalysisComponent(global, this))
- val descriptions = List[String]("funcheck analyses")
-}
diff --git a/src/main/scala/purescala/AbstractZ3Solver.scala b/src/main/scala/leon/AbstractZ3Solver.scala
similarity index 65%
rename from src/main/scala/purescala/AbstractZ3Solver.scala
rename to src/main/scala/leon/AbstractZ3Solver.scala
index 771dc934df3d472f599066e5ba2f7f03b78a20c7..5c1fc48fa9b223cfeb134ad4920296e520d58129 100644
--- a/src/main/scala/purescala/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/AbstractZ3Solver.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -19,29 +19,29 @@ trait AbstractZ3Solver {
class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
- protected[purescala] var z3 : Z3Context
- protected[purescala] var program : Program
+ protected[leon] var z3 : Z3Context
+ protected[leon] var program : Program
def typeToSort(tt: TypeTree): Z3Sort
- protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl]
- protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
- protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
+ protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl]
+ protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
+ protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
- protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort]
- protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort]
+ protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] var funSorts: Map[TypeTree, Z3Sort]
- protected[purescala] var funDomainConstructors: Map[TypeTree, Z3FuncDecl]
- protected[purescala] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]]
+ protected[leon] var funSorts: Map[TypeTree, Z3Sort]
+ protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl]
+ protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]]
- protected[purescala] var exprToZ3Id : Map[Expr,Z3AST]
- protected[purescala] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree]) : Expr
+ protected[leon] var exprToZ3Id : Map[Expr,Z3AST]
+ protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree]) : Expr
- protected[purescala] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
+ protected[leon] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
try {
Some(fromZ3Formula(model, tree, Some(expectedType)))
} catch {
@@ -49,9 +49,9 @@ trait AbstractZ3Solver {
}
}
- protected[purescala] def solveWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr])
+ protected[leon] def solveWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr])
- protected[purescala] def boundValues : Unit = {
+ protected[leon] def boundValues : Unit = {
val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
diff --git a/src/main/scala/purescala/Analysis.scala b/src/main/scala/leon/Analysis.scala
similarity index 98%
rename from src/main/scala/purescala/Analysis.scala
rename to src/main/scala/leon/Analysis.scala
index cd2a97b463c1915f569d02d2ba6f6ba2edd3f7dd..9849330cedf1a3d48c0eabd8cff0508a4a01b8b3 100644
--- a/src/main/scala/purescala/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -1,9 +1,9 @@
-package purescala
+package leon
-import Common._
-import Definitions._
-import Trees._
-import TypeTrees._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/funcheck/Annotations.scala b/src/main/scala/leon/Annotations.scala
similarity index 86%
rename from src/main/scala/funcheck/Annotations.scala
rename to src/main/scala/leon/Annotations.scala
index c90e43247bb89039571373cf7d3321f808a16c2d..0831c8ff81ae212d6e0fd10d5a847c77c88186f4 100644
--- a/src/main/scala/funcheck/Annotations.scala
+++ b/src/main/scala/leon/Annotations.scala
@@ -1,4 +1,4 @@
-package funcheck
+package leon
object Annotations {
class induct extends StaticAnnotation
diff --git a/src/main/scala/purescala/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
similarity index 99%
rename from src/main/scala/purescala/DefaultTactic.scala
rename to src/main/scala/leon/DefaultTactic.scala
index 7a212b667d54e2e42f1662c8a5044d26cb3ef34e..6f31b9ff59bc4b4681e7284c4dc3479400585534 100644
--- a/src/main/scala/purescala/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
import purescala.Common._
import purescala.Trees._
diff --git a/src/main/scala/purescala/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
similarity index 99%
rename from src/main/scala/purescala/Evaluator.scala
rename to src/main/scala/leon/Evaluator.scala
index ebaea193ee660b0adb5a9e343ed185036aa40258..aec3acfa1c0c20c797f0284b09ebb99f25a08a67 100644
--- a/src/main/scala/purescala/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -1,8 +1,8 @@
-package purescala
+package leon
-import Common._
-import Trees._
-import TypeTrees._
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
object Evaluator {
// Expr should be some ground term. We have call-by-value semantics.
diff --git a/src/main/scala/purescala/Extensions.scala b/src/main/scala/leon/Extensions.scala
similarity index 99%
rename from src/main/scala/purescala/Extensions.scala
rename to src/main/scala/leon/Extensions.scala
index 8bc5a4c4673c0688ea9a1364dc02b5af18dddb67..5905ec99820c7dff51cef6fef88705017a17614d 100644
--- a/src/main/scala/purescala/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
import purescala.Trees._
import purescala.Definitions._
diff --git a/src/main/scala/purescala/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
similarity index 97%
rename from src/main/scala/purescala/FairZ3Solver.scala
rename to src/main/scala/leon/FairZ3Solver.scala
index d4208a8dd8a08b3d3a802942535c3925276bbbaf..390a72ee9e5a41f9872ee1a10b50d56d893e27dd 100644
--- a/src/main/scala/purescala/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -31,8 +31,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
)
toggleWarningMessages(true)
- protected[purescala] var z3: Z3Context = null
- protected[purescala] var program: Program = null
+ protected[leon] var z3: Z3Context = null
+ protected[leon] var program: Program = null
private var neverInitialized = true
private var unrollingBank: UnrollingBank = null
@@ -98,9 +98,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[purescala] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[purescala] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
- protected[purescala] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+ protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
private var intSetMinFun: Z3FuncDecl = null
private var intSetMaxFun: Z3FuncDecl = null
@@ -108,20 +108,20 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty
private var fallbackSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
- protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
- protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
+ protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
+ protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
+ protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
private var reverseADTTesters: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
- protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
- protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
+ protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
private def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
case Some(z3sort) => z3sort
@@ -817,9 +817,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(cleanedUp, newClauses.reverse, ite2Bools)
}
- protected[purescala] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
- protected[purescala] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
- protected[purescala] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
+ protected[leon] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
+ protected[leon] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
+ protected[leon] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
class CantTranslateException extends Exception
val varsInformula: Set[Identifier] = variablesOf(expr)
@@ -1007,7 +1007,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
- protected[purescala] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
+ protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
def rec(t: Z3AST, expType: Option[TypeTree] = None) : Expr = expType match {
case Some(MapType(kt,vt)) =>
model.getArrayValue(t) match {
diff --git a/src/main/scala/purescala/FunctionTemplate.scala b/src/main/scala/leon/FunctionTemplate.scala
similarity index 97%
rename from src/main/scala/purescala/FunctionTemplate.scala
rename to src/main/scala/leon/FunctionTemplate.scala
index e8f1e0667941227954cb1d8465f8b171e3d2784b..6a4395f188bf19d7b636c3cb3ec646d921ed38b1 100644
--- a/src/main/scala/purescala/FunctionTemplate.scala
+++ b/src/main/scala/leon/FunctionTemplate.scala
@@ -1,12 +1,13 @@
-package purescala
+package leon
-import Common._
-import Trees._
-import TypeTrees._
-import Definitions._
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.Definitions._
import scala.collection.mutable.{Set=>MutableSet,Map=>MutableMap}
+// TODO: maybe a candidate for moving into purescala package?
class FunctionTemplate private(
funDef : FunDef,
activatingBool : Identifier,
diff --git a/src/main/scala/purescala/InductionTactic.scala b/src/main/scala/leon/InductionTactic.scala
similarity index 99%
rename from src/main/scala/purescala/InductionTactic.scala
rename to src/main/scala/leon/InductionTactic.scala
index d93cc5957327f317dcf354dd8ea8413848d086e6..5e14f196318a74a53761f17dd9a8b06bd9c63f78 100644
--- a/src/main/scala/purescala/InductionTactic.scala
+++ b/src/main/scala/leon/InductionTactic.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
import purescala.Common._
import purescala.Trees._
diff --git a/src/main/scala/purescala/ParallelSolver.scala b/src/main/scala/leon/ParallelSolver.scala
similarity index 96%
rename from src/main/scala/purescala/ParallelSolver.scala
rename to src/main/scala/leon/ParallelSolver.scala
index 63b04c76ccc4a21354d6ebe6cf94a9d7faf3395f..1a3e1d7c4e43ef7f397f42b10d2460eeb4c45ff3 100644
--- a/src/main/scala/purescala/ParallelSolver.scala
+++ b/src/main/scala/leon/ParallelSolver.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import Evaluator._
diff --git a/src/main/scala/purescala/RandomSolver.scala b/src/main/scala/leon/RandomSolver.scala
similarity index 97%
rename from src/main/scala/purescala/RandomSolver.scala
rename to src/main/scala/leon/RandomSolver.scala
index 2b0efd49d5b0d27419065de15bb7f74e2fc57b52..f153818924cd47d79f7470b8487767df5f30f7bc 100644
--- a/src/main/scala/purescala/RandomSolver.scala
+++ b/src/main/scala/leon/RandomSolver.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import Evaluator._
diff --git a/src/main/scala/purescala/Reporter.scala b/src/main/scala/leon/Reporter.scala
similarity index 98%
rename from src/main/scala/purescala/Reporter.scala
rename to src/main/scala/leon/Reporter.scala
index ed41c8beb628ee8ed93631db104536c4097f4e87..71f22363a9cc7f62848971617625ac8ee7f7704f 100644
--- a/src/main/scala/purescala/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -1,7 +1,8 @@
-package purescala
+package leon
import purescala.Definitions.Definition
import purescala.Trees.Expr
+import purescala.PrettyPrinter
abstract class Reporter {
def error(msg: Any) : Unit
diff --git a/src/main/scala/purescala/Settings.scala b/src/main/scala/leon/Settings.scala
similarity index 98%
rename from src/main/scala/purescala/Settings.scala
rename to src/main/scala/leon/Settings.scala
index 914f9c0bd51f61514d49c9ea001f9f6d2ff5f480..d62dd80d241e1dbdded051234169f8ab06f91c01 100644
--- a/src/main/scala/purescala/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
// typically these settings can be changed through some command-line switch.
object Settings {
diff --git a/src/main/scala/purescala/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
similarity index 98%
rename from src/main/scala/purescala/Stopwatch.scala
rename to src/main/scala/leon/Stopwatch.scala
index c56d17626385cdd7643e1f5d85ce9cb58e9d0103..842e3fc0a6989d7ff58c69467a7df7f32132651f 100644
--- a/src/main/scala/purescala/Stopwatch.scala
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
/** Implements a stopwatch for profiling purposes */
class Stopwatch(description : String, verbose : Boolean = false) {
diff --git a/src/main/scala/purescala/TestExtension.scala b/src/main/scala/leon/TestExtension.scala
similarity index 98%
rename from src/main/scala/purescala/TestExtension.scala
rename to src/main/scala/leon/TestExtension.scala
index f4244f1a96f0539792282e690f3c83074778149b..c76f81caf5aec469c7b22a1de442e01a83236674 100644
--- a/src/main/scala/purescala/TestExtension.scala
+++ b/src/main/scala/leon/TestExtension.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
import purescala.Common._
import purescala.Trees._
import purescala.TypeTrees._
import purescala.Definitions._
-import purescala.Extensions._
+import Extensions._
class TestExtension(val reporter: Reporter) extends Analyser(reporter) {
val description : String = "Testing."
diff --git a/src/main/scala/purescala/TimeoutSolver.scala b/src/main/scala/leon/TimeoutSolver.scala
similarity index 83%
rename from src/main/scala/purescala/TimeoutSolver.scala
rename to src/main/scala/leon/TimeoutSolver.scala
index dcd2a95adba7c29b9db22ef5de05cb511d3f5bcc..1785aec5ecc0be3dfc88d9b06a927d86e4e4f3a1 100644
--- a/src/main/scala/purescala/TimeoutSolver.scala
+++ b/src/main/scala/leon/TimeoutSolver.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import scala.sys.error
diff --git a/src/main/scala/purescala/Timer.scala b/src/main/scala/leon/Timer.scala
similarity index 97%
rename from src/main/scala/purescala/Timer.scala
rename to src/main/scala/leon/Timer.scala
index b72b12b3e7076eb42588834e4db6d1565aabfc4f..ffc9d2c5b304951672d357665878e624f19ac966 100644
--- a/src/main/scala/purescala/Timer.scala
+++ b/src/main/scala/leon/Timer.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
/** Creates a thread that, when started, counts for maxsecs seconds and then
* calls the callback, unless the timer was halted first. */
diff --git a/src/main/scala/purescala/TrivialSolver.scala b/src/main/scala/leon/TrivialSolver.scala
similarity index 81%
rename from src/main/scala/purescala/TrivialSolver.scala
rename to src/main/scala/leon/TrivialSolver.scala
index 78cf3d0ef3117305c85d42d6bc9f556cd2d4c474..7e08c483237aa6649c9da425d6e0c58c7b9301aa 100644
--- a/src/main/scala/purescala/TrivialSolver.scala
+++ b/src/main/scala/leon/TrivialSolver.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
val description = "Solver for syntactically trivial formulas"
diff --git a/src/main/scala/funcheck/Utils.scala b/src/main/scala/leon/Utils.scala
similarity index 92%
rename from src/main/scala/funcheck/Utils.scala
rename to src/main/scala/leon/Utils.scala
index a88bc888a97eb8138ad9acde7143eb5d7e932f07..6d7f019ce669a9e81f7da0380048d0071d6713bc 100644
--- a/src/main/scala/funcheck/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -1,4 +1,4 @@
-package funcheck
+package leon
object Utils {
sealed class IsValid(val property : Boolean) {
diff --git a/src/main/scala/purescala/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
similarity index 94%
rename from src/main/scala/purescala/VerificationCondition.scala
rename to src/main/scala/leon/VerificationCondition.scala
index 7c6710fa2c1ae1b30109ddc16a832d6316bbe8ff..4150536fa441352761a7542019caa64d478b0d6a 100644
--- a/src/main/scala/purescala/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -1,9 +1,9 @@
-package purescala
+package leon
+import purescala.Trees._
+import purescala.Definitions._
+import purescala.Common._
import Extensions._
-import Trees._
-import Definitions._
-import Common._
/** This is just to hold some history information. */
class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends ScalacPositional {
diff --git a/src/main/scala/purescala/Z3ModelReconstruction.scala b/src/main/scala/leon/Z3ModelReconstruction.scala
similarity index 95%
rename from src/main/scala/purescala/Z3ModelReconstruction.scala
rename to src/main/scala/leon/Z3ModelReconstruction.scala
index 59fea83e16667501e45af814134a0233957d09f5..913da2fa32b64056026f24e3d1ea1cbd8dd81672 100644
--- a/src/main/scala/purescala/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/Z3ModelReconstruction.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
trait Z3ModelReconstruction {
self: AbstractZ3Solver =>
diff --git a/src/main/scala/purescala/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
similarity index 99%
rename from src/main/scala/purescala/isabelle/Main.scala
rename to src/main/scala/leon/isabelle/Main.scala
index 48ce2afdbc0e1b8392b73375b4b197d8da2dd440..3fd96cff3553e8893dce9b9ba0e24609796c6685 100644
--- a/src/main/scala/purescala/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -1,12 +1,14 @@
-package purescala.isabelle
-import purescala.Reporter
-import purescala.Trees._
-import purescala.Definitions._
-import purescala.Extensions._
-import purescala.Settings._
-import purescala.Common.Identifier
-import purescala.TypeTrees._
-import purescala.PrettyPrinter
+package leon.isabelle
+
+import leon.Extensions._
+import leon.Reporter
+import leon.Settings._
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Definitions._
+import leon.purescala.PrettyPrinter
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
import java.lang.StringBuffer
import java.io._
diff --git a/src/main/scala/purescala/isabelle/README b/src/main/scala/leon/isabelle/README
similarity index 100%
rename from src/main/scala/purescala/isabelle/README
rename to src/main/scala/leon/isabelle/README
diff --git a/src/main/scala/purescala/isabelle/StrongConnectedComponents.scala b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
similarity index 95%
rename from src/main/scala/purescala/isabelle/StrongConnectedComponents.scala
rename to src/main/scala/leon/isabelle/StrongConnectedComponents.scala
index d7a5991da5bffb44a455cbe8894b8ca7fd8e3413..78eb355ff9f64f42213adaa43028eb2e999bdedb 100644
--- a/src/main/scala/purescala/isabelle/StrongConnectedComponents.scala
+++ b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
@@ -1,12 +1,14 @@
-package purescala.isabelle
-import purescala.Reporter
-import purescala.Trees._
-import purescala.Definitions._
-import purescala.Extensions._
-import purescala.Settings._
-import purescala.Common.Identifier
-import purescala.TypeTrees._
-import purescala.PrettyPrinter
+package leon.isabelle
+
+import leon.Extensions._
+import leon.Reporter
+import leon.Settings._
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Definitions._
+import leon.purescala.PrettyPrinter
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
import java.lang.StringBuffer
import java.io._
diff --git a/src/main/scala/funcheck/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
similarity index 89%
rename from src/main/scala/funcheck/AnalysisComponent.scala
rename to src/main/scala/leon/plugin/AnalysisComponent.scala
index 7ca519621e2e0c794a922eeb481b11205f57e1e7..7756946ad0ad11a87560d6bc1bb42882d3765469 100644
--- a/src/main/scala/funcheck/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -1,9 +1,10 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc._
import scala.tools.nsc.plugins._
-class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
+class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
extends PluginComponent
with CodeExtraction
{
@@ -15,7 +16,7 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
val phaseName = pluginInstance.name
- /** this is initialized when the Funcheck phase starts*/
+ /** this is initialized when the Leon phase starts*/
var fresh: scala.tools.nsc.util.FreshNameCreator = null
protected def stopIfErrors: Unit = {
@@ -39,14 +40,14 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
sys.exit(0)
} else {
if(!pluginInstance.actionAfterExtraction.isDefined) {
- println("Extracted program for " + unit + ". Re-run with -P:funcheck:parse to see the output.")
+ println("Extracted program for " + unit + ". Re-run with -P:leon:parse to see the output.")
}
//println(prog)
}
if(!pluginInstance.actionAfterExtraction.isDefined) {
println("Starting analysis.")
- val analysis = new purescala.Analysis(prog)
+ val analysis = new Analysis(prog)
analysis.analyse
if(pluginInstance.stopAfterAnalysis) {
println("Analysis complete. Now terminating the compiler process.")
diff --git a/src/main/scala/funcheck/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
similarity index 99%
rename from src/main/scala/funcheck/CodeExtraction.scala
rename to src/main/scala/leon/plugin/CodeExtraction.scala
index af9756e60bb900fcbbdd4f75fd6678e5cbf5a30b..1930fc7a0507f8d12451c127448a53b9089aa233 100644
--- a/src/main/scala/funcheck/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -1,4 +1,5 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc._
import scala.tools.nsc.plugins._
@@ -188,8 +189,8 @@ trait CodeExtraction extends Extractors {
if(mods.isPrivate) funDef.addAnnotation("private")
for(a <- dd.symbol.annotations) {
a.atp.safeToString match {
- case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
- case "funcheck.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+ case "leon.Annotations.induct" => funDef.addAnnotation("induct")
+ case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
case _ => ;
}
}
diff --git a/src/main/scala/funcheck/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
similarity index 99%
rename from src/main/scala/funcheck/Extractors.scala
rename to src/main/scala/leon/plugin/Extractors.scala
index ff7791bae9c595e462da725b571bd8110da0ea22..ee684e97a56cd4e639958b67f9957d4bf2e751b0 100644
--- a/src/main/scala/funcheck/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -1,11 +1,12 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc._
/** Contains extractors to pull-out interesting parts of the Scala ASTs. */
trait Extractors {
val global: Global
- val pluginInstance: FunCheckPlugin
+ val pluginInstance: LeonPlugin
import global._
import global.definitions._
@@ -45,7 +46,7 @@ trait Extractors {
object ExHoldsExpression {
def unapply(tree: Select) : Option[Tree] = tree match {
- case Select(Apply(Select(Select(funcheckIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (
+ case Select(Apply(Select(Select(leonIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (
utilsName.toString == "Utils" &&
any2IsValidName.toString == "any2IsValid" &&
holdsName.toString == "holds") => Some(realExpr)
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
new file mode 100644
index 0000000000000000000000000000000000000000..39356927db6f25774de59f175ef2d8167f4a60ae
--- /dev/null
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -0,0 +1,80 @@
+package leon
+package plugin
+
+import scala.tools.nsc
+import scala.tools.nsc.{Global,Phase}
+import scala.tools.nsc.plugins.{Plugin,PluginComponent}
+import purescala.Definitions.Program
+
+/** This class is the entry point for the plugin. */
+class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=>Unit] = None) extends Plugin {
+ import global._
+
+ val name = "leon"
+ val description = "The Leon static analyzer"
+
+ var stopAfterAnalysis: Boolean = true
+ var stopAfterExtraction: Boolean = false
+ var silentlyTolerateNonPureBodies: Boolean = false
+
+ /** The help message displaying the options for that plugin. */
+ override val optionsHelp: Option[String] = Some(
+ " -P:leon:uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
+ " -P:leon:with-code Allows the compiler to keep running after the static analysis" + "\n" +
+ " -P:leon:parse Checks only whether the program is valid PureScala" + "\n" +
+ " -P:leon:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
+ " -P:leon:nodefaults Runs only the analyses provided by the extensions" + "\n" +
+ " -P:leon:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
+ " -P:leon:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
+ " -P:leon:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
+ " -P:leon:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
+ " -P:leon:bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
+ " -P:leon:impure Generate testcases only for impure functions" + "\n" +
+ " -P:leon:testcases=[1,2] Number of testcases to generate per function" + "\n" +
+ " -P:leon:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
+ " -P:leon:timeout=N Sets a timeout of N seconds" + "\n" +
+ " -P:leon:XP Enable weird transformations and other bug-producing features" + "\n" +
+ " -P:leon:BV Use bit-vectors for integers" + "\n" +
+ " -P:leon:prune Use additional SMT queries to rule out some unrollings" + "\n" +
+ " -P:leon:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
+ " -P:leon:quickcheck Use QuickCheck-like random search" + "\n" +
+ " -P:leon:parallel Run all solvers in parallel" + "\n" +
+ " -P:leon:templates Use new ``FunctionTemplate'' technique" + "\n" +
+ " -P:leon:noLuckyTests Do not perform additional tests to potentially find models early"
+ )
+
+ /** Processes the command-line options. */
+ private def splitList(lst: String) : Seq[String] = lst.split(':').map(_.trim).filter(!_.isEmpty)
+ override def processOptions(options: List[String], error: String => Unit) {
+ for(option <- options) {
+ option match {
+ case "with-code" => stopAfterAnalysis = false
+ case "uniqid" => leon.Settings.showIDs = true
+ case "parse" => stopAfterExtraction = true
+ case "tolerant" => silentlyTolerateNonPureBodies = true
+ case "nodefaults" => leon.Settings.runDefaultExtensions = false
+ case "axioms" => leon.Settings.noForallAxioms = false
+ case "bapa" => leon.Settings.useBAPA = true
+ case "impure" => leon.Settings.impureTestcases = true
+ case "XP" => leon.Settings.experimental = true
+ case "BV" => leon.Settings.bitvectorBitwidth = Some(32)
+ case "prune" => leon.Settings.pruneBranches = true
+ case "cores" => leon.Settings.useCores = true
+ case "quickcheck" => leon.Settings.useQuickCheck = true
+ case "parallel" => leon.Settings.useParallel = true
+ case "templates" => leon.Settings.useTemplates = true
+ case "noLuckyTests" => leon.Settings.luckyTest = false
+ case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
+ case s if s.startsWith("functions=") => leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
+ case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
+ case s if s.startsWith("testbounds=") => leon.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
+ case s if s.startsWith("timeout=") => leon.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
+ case s if s.startsWith("testcases=") => leon.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
+ case _ => error("Invalid option: " + option)
+ }
+ }
+ }
+
+ val components = List[PluginComponent](new AnalysisComponent(global, this))
+ val descriptions = List[String]("leon analyses")
+}
diff --git a/src/main/scala/funcheck/Main.scala b/src/main/scala/leon/plugin/Main.scala
similarity index 80%
rename from src/main/scala/funcheck/Main.scala
rename to src/main/scala/leon/plugin/Main.scala
index 9266ccff24e925330515a54bad8b73fd02c4bed5..027b35a70572f345567122803aa9fd1ca7a5f0e6 100644
--- a/src/main/scala/funcheck/Main.scala
+++ b/src/main/scala/leon/plugin/Main.scala
@@ -1,12 +1,12 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc.{Global,Settings,SubComponent,CompilerCommand}
import purescala.Definitions.Program
object Main {
- import purescala.{Reporter,DefaultReporter,Definitions,Analysis}
- import Definitions.Program
+ import leon.{Reporter,DefaultReporter,Analysis}
def main(args : Array[String]) : Unit = run(args)
@@ -37,9 +37,9 @@ object Main {
}
private def runWithSettings(args : Array[String], settings : Settings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
- val (funcheckOptions, nonfuncheckOptions) = args.toList.partition(_.startsWith("--"))
- val command = new CompilerCommand(nonfuncheckOptions, settings) {
- override val cmdName = "funcheck"
+ val (leonOptions, nonLeonOptions) = args.toList.partition(_.startsWith("--"))
+ val command = new CompilerCommand(nonLeonOptions, settings) {
+ override val cmdName = "leon"
}
if(command.ok) {
@@ -47,9 +47,8 @@ object Main {
println(command.cmdName + " beta.")
} else {
val runner = new PluginRunner(settings, printerFunction, actionOnProgram)
- runner.funcheckPlugin.processOptions(funcheckOptions.map(_.substring(2)), Console.err.println(_))
- //runner.funcheckPlugin.stopAfterExtraction = false
- runner.funcheckPlugin.stopAfterAnalysis = false
+ runner.leonPlugin.processOptions(leonOptions.map(_.substring(2)), Console.err.println(_))
+ runner.leonPlugin.stopAfterAnalysis = false
val run = new runner.Run
run.compile(command.files)
}
@@ -60,7 +59,7 @@ object Main {
/** This class is a compiler that will be used for running the plugin in
* standalone mode. Original version courtesy of D. Zufferey. */
class PluginRunner(settings : Settings, reportingFunction : String => Unit, actionOnProgram : Option[Program=>Unit]) extends Global(settings, new SimpleReporter(settings, reportingFunction)) {
- val funcheckPlugin = new FunCheckPlugin(this, actionOnProgram)
+ val leonPlugin = new LeonPlugin(this, actionOnProgram)
protected def myAddToPhasesSet(sub : SubComponent, descr : String) : Unit = {
phasesSet += sub
@@ -77,7 +76,7 @@ class PluginRunner(settings : Settings, reportingFunction : String => Unit, acti
pickler -> "serialize symbol tables",
refchecks -> "reference and override checking, translate nested objects"
) ::: {
- val zipped = funcheckPlugin.components zip funcheckPlugin.descriptions
+ val zipped = leonPlugin.components zip leonPlugin.descriptions
zipped
}
phs foreach (myAddToPhasesSet _).tupled
diff --git a/src/main/scala/funcheck/SimpleReporter.scala b/src/main/scala/leon/plugin/SimpleReporter.scala
similarity index 98%
rename from src/main/scala/funcheck/SimpleReporter.scala
rename to src/main/scala/leon/plugin/SimpleReporter.scala
index cd20fd8c53a35e7e496a3e6727e95927b505b163..0d8e4b0adf6d93d355c5bfaf57f49916b630851b 100644
--- a/src/main/scala/funcheck/SimpleReporter.scala
+++ b/src/main/scala/leon/plugin/SimpleReporter.scala
@@ -1,4 +1,5 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc.Settings
import scala.tools.nsc.reporters.AbstractReporter
diff --git a/src/main/scala/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
similarity index 98%
rename from src/main/scala/purescala/Common.scala
rename to src/main/scala/leon/purescala/Common.scala
index f3e95df309b860469bd9a3fe821b8744b7041630..6132bd607724a4b9273ad199545e46cfe2adb368 100644
--- a/src/main/scala/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
object Common {
@@ -18,7 +19,7 @@ object Common {
override def hashCode: Int = id
override def toString: String = {
- if(purescala.Settings.showIDs) {
+ if(Settings.showIDs) {
// angle brackets: name + "\u3008" + id + "\u3009"
name + "[" + id + "]"
} else if(alwaysShowUniqueID) {
diff --git a/src/main/scala/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
similarity index 99%
rename from src/main/scala/purescala/Definitions.scala
rename to src/main/scala/leon/purescala/Definitions.scala
index 5aa535395f095d4477e3b0f83d5b4af385618b49..efd8b52fb31e7cd4d61ff868bba3c836ca1f0e2e 100644
--- a/src/main/scala/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
object Definitions {
diff --git a/src/main/scala/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
similarity index 99%
rename from src/main/scala/purescala/PrettyPrinter.scala
rename to src/main/scala/leon/purescala/PrettyPrinter.scala
index 16d811e913df7497f0530bd15f829bee19a53958..c5d2d7158ecd416ea8d25ecfaa84e0ecc882830f 100644
--- a/src/main/scala/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -1,6 +1,6 @@
+package leon
package purescala
-
/** This pretty-printer uses Unicode for some operators, to make sure we
* distinguish PureScala from "real" Scala (and also because it's cute). */
object PrettyPrinter {
diff --git a/src/main/scala/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
similarity index 99%
rename from src/main/scala/purescala/Trees.scala
rename to src/main/scala/leon/purescala/Trees.scala
index 338b5d24ac10fd6ab014fbd6a42a019cf67a85c3..7a289934acf62f1cdd94c4341455722e6edd3290 100644
--- a/src/main/scala/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
/** AST definitions for Pure Scala. */
diff --git a/src/main/scala/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
similarity index 99%
rename from src/main/scala/purescala/TypeTrees.scala
rename to src/main/scala/leon/purescala/TypeTrees.scala
index eab21e5cb9219832fe3a54a321c7de79bdc550f7..e948a433f42e58cb452877414fada6fae5f8da5d 100644
--- a/src/main/scala/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
object TypeTrees {
diff --git a/src/main/scala/purescala/z3plugins/bapa/AST.scala b/src/main/scala/leon/z3plugins/bapa/AST.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/AST.scala
rename to src/main/scala/leon/z3plugins/bapa/AST.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/BAPATheory.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/BAPATheory.scala
rename to src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/BAPATheoryBubbles.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/BAPATheoryBubbles.scala
rename to src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/BAPATheoryEqc.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/BAPATheoryEqc.scala
rename to src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/Bubbles.scala b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/Bubbles.scala
rename to src/main/scala/leon/z3plugins/bapa/Bubbles.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/NormalForms.scala b/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/NormalForms.scala
rename to src/main/scala/leon/z3plugins/bapa/NormalForms.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/PrettyPrinter.scala b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/PrettyPrinter.scala
rename to src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/VennRegions.scala b/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/VennRegions.scala
rename to src/main/scala/leon/z3plugins/bapa/VennRegions.scala
diff --git a/testcases/sas2011-testcases/ListOperations.scala b/testcases/sas2011-testcases/ListOperations.scala
index 3a08ac8f916661e89e2455eeaa2edf0593765f7e..a4fc4f8dc44a90f59a772b52b1a05053316e94d2 100644
--- a/testcases/sas2011-testcases/ListOperations.scala
+++ b/testcases/sas2011-testcases/ListOperations.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object ListOperations {
sealed abstract class List