From b9ba429d0c6933d4065634a20ccaaf58e02bd8f0 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 31 Mar 2014 19:41:53 +0200
Subject: [PATCH] Support for internal errors
---
src/main/scala/leon/Reporter.scala | 20 +++++++++++++++++---
1 file changed, 17 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 18e93f870..a8373bdd2 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -16,6 +16,7 @@ abstract class Reporter(settings: Settings) {
case object WARNING extends Severity
case object ERROR extends Severity
case object FATAL extends Severity
+ case object INTERNAL extends Severity
case class DEBUG(section: DebugSection) extends Severity
case class Message(severity: Severity, position: Position, msg: Any);
@@ -28,9 +29,9 @@ abstract class Reporter(settings: Settings) {
def account(msg: Message): Message = {
msg.severity match {
- case WARNING => _warningCount += 1
- case ERROR | FATAL => _errorCount += 1
- case _ =>
+ case WARNING => _warningCount += 1
+ case ERROR | FATAL | INTERNAL => _errorCount += 1
+ case _ =>
}
msg
@@ -50,6 +51,15 @@ abstract class Reporter(settings: Settings) {
emit(account(Message(FATAL, pos, msg)))
onFatal()
}
+ final def internalError(pos: Position, msg : Any) : Nothing = {
+ emit(account(Message(INTERNAL, pos, msg.toString +
+ "\nPlease inform the authors of Leon about this message"
+ )))
+ onFatal()
+ }
+ final def internalAssertion(cond : Boolean, pos: Position, msg : Any) : Unit = {
+ if (!cond) internalError(pos,msg)
+ }
def terminateIfError() = {
if (errorCount > 0) {
@@ -87,6 +97,8 @@ abstract class Reporter(settings: Settings) {
final def warning(msg: Any): Unit = warning(NoPosition, msg)
final def error(msg: Any): Unit = error(NoPosition, msg)
final def fatalError(msg: Any): Nothing = fatalError(NoPosition, msg)
+ final def internalError(msg: Any) : Nothing = internalError(NoPosition, msg)
+ final def internalAssertion(cond : Boolean, msg: Any) : Unit = internalAssertion(cond,NoPosition, msg)
final def debug(msg: => Any)(implicit section: DebugSection): Unit = debug(NoPosition, msg)
}
@@ -96,6 +108,7 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
case WARNING => "["+Console.YELLOW +"Warning"+Console.RESET+"]"
case INFO => "["+Console.BLUE +" Info "+Console.RESET+"]"
case FATAL => "["+Console.RED+Console.BOLD +" Fatal "+Console.RESET+"]"
+ case INTERNAL => "["+ Console.BOLD +"Internal"+Console.RESET+"]"
case DEBUG(_) => "["+Console.MAGENTA +" Debug "+Console.RESET+"]"
}
@@ -163,4 +176,5 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
protected def reline(pfx: String, msg: String) : String = {
pfx+" "+msg.replaceAll("\n", "\n" + (" " * prefixSize))
}
+
}
--
GitLab