From e0482187a814ca25210cb2cca29fdf791c71c46f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 1 Apr 2015 13:13:25 +0200
Subject: [PATCH] Extract ensuring(expr: Boolean) as ensuring(res => expr)
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 9 ++++++++-
.../purescala/invalid/EnsuringBoolean.scala | 10 ++++++++++
2 files changed, 18 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 8d6c9cef9..9a80528f3 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1064,7 +1064,14 @@ trait CodeExtraction extends ASTExtractors {
NoTree(toPureScalaType(current.tpe)(dctx, current.pos))
}
- Ensuring(b, post)
+ val closure = post.getType match {
+ case BooleanType =>
+ val resId = FreshIdentifier("res", BooleanType).setPos(post).setOwner(currentFunDef)
+ Lambda(Seq(LeonValDef(resId)), post).setPos(post)
+ case _ => post
+ }
+
+ Ensuring(b, closure)
case t @ ExHoldsExpression(body) =>
val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos).setOwner(currentFunDef)
diff --git a/src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala b/src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala
new file mode 100644
index 000000000..8d9c793b5
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala
@@ -0,0 +1,10 @@
+import leon._
+import leon.lang._
+import leon.annotation._
+import scala.language.postfixOps
+object EnsuringBoolean {
+ def congR(x: BigInt)(implicit mod: BigInt): Unit = {
+ require(mod >= 1);
+ ()
+ } ensuring(false)
+}
--
GitLab