diff --git a/src/funcheck/AbstractPlugin.scala b/src/funcheck/AbstractPlugin.scala
new file mode 100644
index 0000000000000000000000000000000000000000..07847a298f83a8a996c16871c83329fb43e32219
--- /dev/null
+++ b/src/funcheck/AbstractPlugin.scala
@@ -0,0 +1,11 @@
+package funcheck
+
+import scala.tools.nsc
+import scala.tools.nsc.{Global,Phase}
+import scala.tools.nsc.plugins.{Plugin,PluginComponent}
+
+abstract class AbstractPlugin extends Plugin {
+ import global._
+
+ var silentlyTolerateNonPureBodies: Boolean = false
+}
diff --git a/src/funcheck/CPPlugin.scala b/src/funcheck/CPPlugin.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e39cc73d04e103343c4877a764953fbe44775664
--- /dev/null
+++ b/src/funcheck/CPPlugin.scala
@@ -0,0 +1,70 @@
+package funcheck
+
+import scala.tools.nsc
+import scala.tools.nsc.{Global,Phase}
+import scala.tools.nsc.plugins.{Plugin,PluginComponent}
+
+/** This class is the entry point for the plugin. */
+class CPPlugin(val global: Global) extends AbstractPlugin {
+ import global._
+
+ val name = "constraint-programming"
+ val description = "Constraint programming in Scala by LARA."
+
+ var stopAfterAnalysis: Boolean = true
+ var stopAfterExtraction: 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:nobapa Disable BAPA Z3 extension" + "\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:quiet No info and warning messages from the extensions" + "\n" +
+ " -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
+ " -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
+ " -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
+ " -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
+ " -P:funcheck:cores (with CAV) Use UNSAT cores in the unrolling/refinement step."
+ )
+
+ /** 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 "quiet" => purescala.Settings.quietExtensions = true
+ case "nodefaults" => purescala.Settings.runDefaultExtensions = false
+ case "axioms" => purescala.Settings.noForallAxioms = false
+ case "nobapa" => purescala.Settings.useBAPA = false
+ case "impure" => purescala.Settings.impureTestcases = true
+ case "newPM" => { println("''newPM'' is no longer a command-line option, because the new translation is now on by default."); System.exit(0) }
+ case "XP" => purescala.Settings.experimental = true
+ case "PLDI" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useFairInstantiator = false; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
+ case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
+ case "prune" => purescala.Settings.pruneBranches = true
+ case "cores" => purescala.Settings.useCores = true
+ 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("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 CPComponent(global, this))}