diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 254fd8f5777e4859fbca6ae20c8872502e621587..369be0adfbba6ba4dfba7e7229c41785c8ccb4dc 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -236,6 +236,10 @@ trait CodeExtraction extends ASTExtractors { case d @ ExCaseClassSyntheticJunk() => None + case cd: ClassDef => + outOfSubsetError(cd, "Found class that is not an abstract class nor a case class") + None + case other => outOfSubsetError(other, "Expected: top-level object/class.") None diff --git a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala index be51f8b6393efe2ac354694b8977f2e723431fe4..e3f6817b5f75892b9f8953ed95107a4bd439d1e4 100644 --- a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala +++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala @@ -7,6 +7,7 @@ import scala.tools.nsc.Settings import scala.tools.nsc.reporters.AbstractReporter import scala.reflect.internal.util.{Position, NoPosition, FakePos, StringOps} +import utils.{Position => LeonPosition, NoPosition => LeonNoPosition, OffsetPosition => LeonOffsetPosition} /** This implements a reporter that calls the callback with every line that a regular ConsoleReporter would display. */ @@ -28,14 +29,14 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab StringOps.countElementsAsString((severity).count, label(severity)) /** Prints the message. */ - def printMessage(msg: String, severity: Severity) { + def printMessage(msg: String, pos: LeonPosition, severity: Severity) { severity match { case ERROR => - reporter.error(msg) + reporter.error(pos, msg) case WARNING => - reporter.warning(msg) + reporter.warning(pos, msg) case INFO => - reporter.info(msg) + reporter.info(pos, msg) } } @@ -46,13 +47,13 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab else posIn pos match { case FakePos(fmsg) => - printMessage(fmsg+" "+msg, severity) + printMessage(fmsg+" "+msg, LeonNoPosition, severity) case NoPosition => - printMessage(msg, severity) + printMessage(msg, LeonNoPosition, severity) case _ => val buf = new StringBuilder(msg) - val file = pos.source.file - printMessage(pos.line + ": " + msg+"\n"+getSourceLine(pos), severity) + val lpos = LeonOffsetPosition(pos.line, pos.column, pos.point, pos.source.file.file) + printMessage(msg+"\n"+getSourceLine(pos), lpos, severity) } } def print(pos: Position, msg: String, severity: Severity) { @@ -70,8 +71,8 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab } def printSummary() { - if (WARNING.count > 0) printMessage(getCountString(WARNING) + " found", INFO) - if ( ERROR.count > 0) printMessage(getCountString(ERROR ) + " found", INFO) + if (WARNING.count > 0) printMessage(getCountString(WARNING) + " found", LeonNoPosition, INFO) + if ( ERROR.count > 0) printMessage(getCountString(ERROR ) + " found", LeonNoPosition, INFO) } def display(pos: Position, msg: String, severity: Severity) {