From ac55292e5e03caa4d229de8c15f8d33304c573e0 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 22 Apr 2016 19:28:34 +0200
Subject: [PATCH] regression test for new extern behaviour
---
.../purescala/valid/SpecWithExtern.scala | 22 +++++++++++++++++++
1 file changed, 22 insertions(+)
create mode 100644 src/test/resources/regression/verification/purescala/valid/SpecWithExtern.scala
diff --git a/src/test/resources/regression/verification/purescala/valid/SpecWithExtern.scala b/src/test/resources/regression/verification/purescala/valid/SpecWithExtern.scala
new file mode 100644
index 000000000..d164fee8f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/SpecWithExtern.scala
@@ -0,0 +1,22 @@
+import leon.annotation._
+
+object SpecWithExtern {
+
+
+ //random between returns any value between l and h.
+ //For execution via scalac, we pick one valid implementation, but
+ //we would like the program to be verified versus any possible
+ //implementation, which should happen thanks to @extern
+ @extern
+ def randomBetween(l: Int, h: Int): Int = {
+ require(l <= h)
+ l
+ } ensuring(res => (res >= l && res <= h))
+
+ //postcondition is wrong, but if leon considers
+ //actual body of randomBetween it would be correct
+ def wrongProp(): Int = {
+ randomBetween(0, 10)
+ } ensuring(res => res >= 0 && res < 10)
+
+}
--
GitLab