From 04efeeddcdd9218bbb426ef634823fa3ac57fa3a Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 22 Oct 2015 11:48:56 +0200
Subject: [PATCH] add some counter-examples as well
---
.../xlang/invalid/NestedFunState1.scala | 20 ++++++++++++++++
.../xlang/invalid/NestedFunState2.scala | 23 +++++++++++++++++++
2 files changed, 43 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
diff --git a/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala b/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
new file mode 100644
index 000000000..9372ea742
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
@@ -0,0 +1,20 @@
+object NestedFunState1 {
+
+ def simpleSideEffect(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def incA(prevA: BigInt): Unit = {
+ require(prevA == a)
+ a += 1
+ } ensuring(_ => a == prevA + 1)
+
+ incA(a)
+ incA(a)
+ incA(a)
+ incA(a)
+ a
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala b/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
new file mode 100644
index 000000000..68769df28
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object NestedFunState2 {
+
+ def sum(n: BigInt): BigInt = {
+ require(n > 0)
+ var i = BigInt(0)
+ var res = BigInt(0)
+
+ def iter(): Unit = {
+ require(res >= i && i >= 0)
+ if(i < n) {
+ i += 1
+ res += i
+ iter()
+ }
+ }
+
+ iter()
+ res
+ } ensuring(_ < 0)
+
+}
--
GitLab