There's a new prefered way of running funcheck:

after sbt package all, run:

./funcheck --CAV yourfile.scala

That's it.

funcheck

-#!/bin/bash
-
-runner="./scalac-funcheck"
-newargs=""
-
-for arg in $@
-do
-    if [ -e ${arg} ]
-    then
-        newargs="${newargs} ${arg}"
-    else
-        newargs="${newargs} -P:funcheck:${arg}"
-    fi
-done
-
-if [ -e ${runner} ]
-then
-    ${runner} ${newargs}
-    exit 0
-else
-    echo "${runner} not found. Have you run 'sbt all' ?"
-    exit 1
-fi
-

project/build/funcheck.scala

@@ -16,7 +16,7 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
 
   lazy val extensionJars : List[Path] = multisetsLib.jarPath :: multisets.jarPath :: orderedsets.jarPath :: setconstraints.jarPath :: Nil
 
-  val scriptPath: Path = "." / "scalac-funcheck"
+  val scriptPath: Path = "." / "funcheck"
 
   lazy val all = task { None } dependsOn(generateScript) describedAs("Compile everything and produce a script file.")
 
@@ -49,14 +49,15 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
       fw.write(purescala.jarPath.absolutePath)
       fw.write("\"" + nl + nl)
       fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl)
-      fw.write("java -Xmx1024M \\" + nl)
+      fw.write("scala -classpath ${FUNCHECKCLASSPATH}:${SCALACCLASSPATH}" + " \\" + nl)
+      fw.write("funcheck.Main -cp " + plugin.jarPath.absolutePath + " $@" + nl)
+      // fw.write("java -Xmx1024M \\" + nl)
+      // // This is a hack :(
+      // val libStr = (buildLibraryJar.absolutePath).toString
+      // fw.write("    -Dscala.home=" + libStr.substring(0, libStr.length-21) + " \\" + nl)
 
-      // This is a hack :(
-      val libStr = (buildLibraryJar.absolutePath).toString
-      fw.write("    -Dscala.home=" + libStr.substring(0, libStr.length-21) + " \\" + nl)
-
-      fw.write("    -classpath ${FUNCHECKCLASSPATH} \\" + nl)
-      fw.write("  scala.tools.nsc.Main -Xplugin:" + plugin.jarPath.absolutePath + " -classpath ${SCALACCLASSPATH} $@" + nl)
+      // fw.write("    -classpath ${FUNCHECKCLASSPATH} \\" + nl)
+      // fw.write("  scala.tools.nsc.Main -Xplugin:" + plugin.jarPath.absolutePath + " -classpath ${SCALACCLASSPATH} $@" + nl)
       fw.close
       f.setExecutable(true)
       None

src/funcheck/DefaultMain.scala

-package funcheck
-
-object DefaultMain {
-  def main(args: Array[String]): Unit = {
-    println("Please use funCheck as a scalac plugin, running:")
-    println("  scalac -Xplugin:funcheck-plugin.jar ...")
-  }
-}

src/funcheck/FunCheckPlugin.scala

@@ -68,4 +68,6 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     }
   }
 
-  val components = List[PluginComponent](new AnalysisComponent(global, this))}
+  val components = List[PluginComponent](new AnalysisComponent(global, this))
+  val descriptions = List[String]("funcheck analyses")
+}

src/funcheck/Main.scala

+package funcheck
+
+import scala.tools.nsc.{Global,Settings,SubComponent,CompilerCommand}
+import scala.tools.nsc.reporters.{ConsoleReporter,Reporter}
+
+/** This class is a compiler that will be used for running
+*  the plugin in standalone mode. Courtesy of D. Zufferey. */
+class PluginRunner(settings : Settings, reporter : Reporter) extends Global(settings, reporter) {
+  def this(settings : Settings) = this(settings, new ConsoleReporter(settings))
+
+    val funcheckPlugin = new FunCheckPlugin(this)
+
+    protected def addToPhasesSet(sub : SubComponent, descr : String) : Unit = {
+    phasesSet += sub
+  }
+
+  /** The phases to be run. */
+  override protected def computeInternalPhases() : Unit = {
+    val phs = List(
+      syntaxAnalyzer          -> "parse source into ASTs, perform simple desugaring",
+      analyzer.namerFactory   -> "resolve names, attach symbols to named trees",
+      analyzer.packageObjects -> "load package objects",
+      analyzer.typerFactory   -> "the meat and potatoes: type the trees",
+      superAccessors          -> "add super accessors in traits and nested classes",
+      pickler                 -> "serialize symbol tables",
+      refchecks               -> "reference and override checking, translate nested objects"
+    ) ::: {
+      val zipped = funcheckPlugin.components zip funcheckPlugin.descriptions
+      zipped
+    }
+    phs foreach (addToPhasesSet _).tupled
+  }
+}
+
+object Main {
+  def main(args: Array[String]): Unit = {
+    val settings = new Settings
+    runWithSettings(args, settings)
+  }
+
+  private def runWithSettings(args : Array[String], settings : Settings) : Unit = {
+    val (funcheckOptions, nonfuncheckOptions) = args.toList.partition(_.startsWith("--"))
+    val command = new CompilerCommand(nonfuncheckOptions, settings) {
+      override val cmdName = "funcheck"
+    }
+
+    if(command.ok) {
+      if(settings.version.value) {
+        println(command.cmdName + " beta.")
+      } else {
+        val runner = new PluginRunner(settings)
+        runner.funcheckPlugin.processOptions(funcheckOptions.map(_.substring(2)), Console.err.println(_))
+        val run = new runner.Run
+        run.compile(command.files)
+      }
+    }
+  }
+}

vstte10competition/SumAndMax.scala

+import scala.collection.immutable.Set
+import funcheck.Utils._
+import funcheck.Annotations._
+
+object SumAndMax {
+  sealed abstract class List
+  case class Cons(head : Int, tail : List) extends List
+  case class Nil() extends List
+
+  def max(list : List) : Int = {
+    require(list != Nil())
+    list match {
+      case Cons(x, Nil()) => x
+      case Cons(x, xs) => {
+        val m2 = max(xs)
+        if(m2 > x) m2 else x
+      }
+    }
+  }
+
+  def sum(list : List) : Int = list match {
+    case Nil() => 0
+    case Cons(x, xs) => x + sum(xs)
+  }
+
+  def size(list : List) : Int = (list match {
+    case Nil() => 0
+    case Cons(_, xs) => 1 + size(xs)
+  }) ensuring(_ >= 0)
+
+  def allPos(list : List) : Boolean = list match {
+    case Nil() => true
+    case Cons(x, xs) => x >= 0 && allPos(xs)
+  }
+
+  def prop0(list : List) : Boolean = {
+    require(list != Nil())
+    !allPos(list) || max(list) >= 0
+  } holds
+
+  @induct
+  def property(list : List) : Boolean = {
+    require(allPos(list))
+    sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
+  } holds
+}