From a99ba210d43feb84782321e9375e431058036576 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 30 Oct 2012 16:45:39 +0100
Subject: [PATCH] Generate leon errors that are explicitly typed
---
library/src/main/scala/leon/Utils.scala | 2 ++
src/main/scala/leon/purescala/ScalaPrinter.scala | 4 +++-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/library/src/main/scala/leon/Utils.scala b/library/src/main/scala/leon/Utils.scala
index a6d1ea771..366cc3975 100644
--- a/library/src/main/scala/leon/Utils.scala
+++ b/library/src/main/scala/leon/Utils.scala
@@ -27,4 +27,6 @@ object Utils {
def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noChoose
def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose
def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose
+
+ def error[T](reason: String): T = sys.error(reason)
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index fb1e14785..feff130ee 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -426,7 +426,9 @@ object ScalaPrinter {
case e @ Error(desc) => {
var nsb = sb
- nsb.append("sys.error(\"" + desc + "\")")
+ nsb.append("leon.Utils.error[")
+ nsb = pp(e.getType, nsb, lvl)
+ nsb.append("](\"" + desc + "\")")
nsb
}
--
GitLab