Block positions, explicit errors from xlang features.

src/main/scala/leon/utils/Positions.scala

@@ -34,6 +34,33 @@ abstract class Position extends Ordered[Position] {
   def isDefined: Boolean
 }
 
+object Position {
+  def between(a: Position, b: Position): Position = {
+    if (a.file == b.file) {
+      if (a.line == b.line && a.col == b.col) {
+        a
+      } else {
+        val (from, to) = if (a < b) (a, b) else (b, a)
+
+        (from, to) match {
+          case (p1: OffsetPosition, p2: OffsetPosition) =>
+            RangePosition(p1.line, p1.col, p1.point, p2.line, p2.col, p2.point, p1.file)
+          case (p1: RangePosition, p2: RangePosition) =>
+            RangePosition(p1.lineFrom, p1.colFrom, p1.pointFrom, p2.lineTo, p2.colTo, p2.pointTo, p1.file)
+          case (p1: OffsetPosition, p2: RangePosition) =>
+            RangePosition(p1.line, p1.col, p1.point, p2.lineTo, p2.colTo, p2.pointTo, p1.file)
+          case (p1: RangePosition, p2: OffsetPosition) =>
+            RangePosition(p1.lineFrom, p1.colFrom, p1.pointFrom, p2.line, p2.col, p2.point, p1.file)
+          case (a,b) =>
+            a
+        }
+      }
+    } else {
+      a
+    }
+  }
+}
+
 abstract class DefinedPosition extends Position {
   override def toString = line+":"+col
   override def fullString = file.getPath+":"+line+":"+col

src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala

@@ -6,11 +6,13 @@ package xlang
 import purescala.Common._
 import purescala.TypeTrees._
 import purescala.Trees._
+import purescala.TreeOps.collect
 import purescala.Definitions._
 import purescala.Constructors._
 
+import utils.Position
+
 import xlang.Trees._
-import xlang.TreeOps.isXLang
 
 object NoXLangFeaturesChecking extends UnitPhase[Program] {
 
@@ -18,11 +20,30 @@ object NoXLangFeaturesChecking extends UnitPhase[Program] {
   val description = "Ensure and enforce that no xlang features are used"
 
   override def apply(ctx: LeonContext, pgm: Program): Unit = {
-    pgm.definedFunctions.foreach(fd => {
-      if(isXLang(fd.fullBody)) {
-        ctx.reporter.fatalError(fd.fullBody.getPos, "Expr is using xlang features")
-      }
-    })
+    val errors = pgm.definedFunctions.flatMap(fd => collect[(Position, String)]{
+      case (e: Block) =>
+        Set((e.getPos, "Block expressions require xlang desugaring"))
+      case (e: Assignment) =>
+        Set((e.getPos, "Mutating variables requires xlang desugaring"))
+      case (e: While) =>
+        Set((e.getPos, "While expressions require xlang desugaring"))
+      case (e: Epsilon) =>
+        Set((e.getPos, "Usage of epsilons requires xlang desugaring"))
+      case (e: EpsilonVariable) =>
+        Set((e.getPos, "Usage of epsilons requires xlang desugaring"))
+      case (e: LetVar) =>
+        Set((e.getPos, "Mutable variables (e.g. 'var x' instead of 'val x') require xlang desugaring"))
+      case (e: Waypoint) =>
+        Set((e.getPos, "Usage of waypoints requires xlang desugaring"))
+      case (e: ArrayUpdate) =>
+        Set((e.getPos, "In-place updates of arrays require xlang desugaring"))
+      case _ =>
+        Set()
+    }(fd.fullBody))
+
+    for ((p, msg) <- errors) {
+      ctx.reporter.error(p, msg)
+    }
   }
 
 }

src/main/scala/leon/xlang/Trees.scala

@@ -24,6 +24,10 @@ object Trees {
       Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
     }
 
+    override def getPos = {
+      Position.between(exprs.head.getPos, last.getPos)
+    }
+
     def printWith(implicit pctx: PrinterContext) {
       p"""|{
           |  ${nary(exprs :+ last, "\n")}