now with a rough filter to weed out many programs containing unsupported stuff

src/funcheck/AnalysisComponent.scala

@@ -19,6 +19,8 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
     import StructuralExtractors._
 
     def apply(unit: CompilationUnit): Unit = {
+      (new ForeachTreeTraverser(firstFilter(unit))).traverse(unit.body)
+      stopIfErrors
       (new ForeachTreeTraverser(findContracts)).traverse(unit.body)
 
       if(pluginInstance.stopAfterAnalysis) {
@@ -27,7 +29,12 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
       }
     }
 
-    def findContracts(tree: Tree): Unit = tree match {
+    private def stopIfErrors: Nothing = {
+      if(reporter.hasErrors) println("There were errors.")
+      exit(0)
+    }
+
+    private def findContracts(tree: Tree): Unit = tree match {
       case DefDef(/*mods*/ _, name, /*tparams*/ _, /*vparamss*/ _, /*tpt*/ _, body) => {
         var realBody = body
         var reqCont: Option[Tree] = None
@@ -51,5 +58,36 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
 
       case _ => ;
     }
+
+    /** Weeds out programs containing unsupported features. */
+    def firstFilter(unit: CompilationUnit)(tree: Tree): Unit = {
+      def unsup(s: String): String = "FunCheck: Unsupported construct: " + s
+
+      tree match {
+        case ClassDef(mods, name, tparams, impl) => {
+          if(mods.isTrait) unit.error(tree.pos, unsup("trait."))
+        }
+
+        case ValDef(mods, name, tpt, rhs) if mods.isVariable =>
+          unit.error(tree.pos, unsup("mutable variable/field."))
+
+        case LabelDef(name, params, rhs) => ;
+           // used for tailcalls and like
+           // while/do are desugared to label defs as follows:
+           // while (cond) body ==> LabelDef($L, List(), if (cond) { body; L$() } else ())
+           // do body while (cond) ==> LabelDef($L, List(), body; if (cond) L$() else ())
+        case Assign(lhs, rhs) => unit.error(tree.pos, unsup("assignment to mutable variable/field."))
+        case Return(expr) => unit.error(tree.pos, unsup("return statement."))
+        case Try(block, catches, finalizer) => unit.error(tree.pos, unsup("try block."))
+        case Throw(expr) => unit.error(tree.pos, unsup("throw statement."))
+        case New(tpt) => unit.error(tree.pos, unsup("'new' operator."))
+        case SingletonTypeTree(ref) => unit.error(tree.pos, unsup("singleton type."))
+        case SelectFromTypeTree(qualifier, selector) => unit.error(tree.pos, unsup("path-dependent type."))
+        case CompoundTypeTree(templ: Template) => unit.error(tree.pos, unsup("compound/refinement type."))
+        case TypeBoundsTree(lo, hi) => unit.error(tree.pos, unsup("type bounds."))
+        case ExistentialTypeTree(tpt, whereClauses) => unit.error(tree.pos, unsup("existential type."))
+        case _ => ;
+      }
+    }
   }
 }