From c0b99138515d015d1b989a97d07ec8a2550edb81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 19 Jul 2012 11:17:36 +0200
Subject: [PATCH] stackoverflow
---
testcases/buggyEpsilon.scala | 81 ++++++++++++++++++++++++++++++++++++
1 file changed, 81 insertions(+)
create mode 100644 testcases/buggyEpsilon.scala
diff --git a/testcases/buggyEpsilon.scala b/testcases/buggyEpsilon.scala
new file mode 100644
index 000000000..b558511a0
--- /dev/null
+++ b/testcases/buggyEpsilon.scala
@@ -0,0 +1,81 @@
+import leon.Utils._
+
+object Test {
+
+ abstract class SortedList
+ case class Cons(head: Int, tail: SortedList) extends SortedList
+ case class Nil() extends SortedList
+
+ def content(l: SortedList): Set[Int] = l match {
+ case Cons(head, tail) => content(tail) ++ Set(head)
+ case Nil() => Set()
+ }
+
+ def insert(x: Int, l: SortedList): SortedList = Cons(x, l)
+
+ def remove(x: Int, l: SortedList): SortedList = {
+ //require(pos(l) && sorted(l, 0))
+ l match {
+ case Cons(head, tail) => if(head == x) remove(x, tail) else if(head < x) Cons(head, remove(x, tail)) else l
+ case Nil() => Nil()
+ }
+ } //ensuring(res => !content(res).contains(x))
+
+ def sorted(l: SortedList, prec: Int): Boolean = l match {
+ case Cons(head, tail) => if(prec <= head) sorted(tail, head) else false
+ case Nil() => true
+ }
+ def pos(l: SortedList): Boolean = l match {
+ case Cons(head, tail) => if(head < 0) false else pos(tail)
+ case Nil() => true
+ }
+
+
+
+ def nonDeterministicList(): Boolean = {
+ var i = 0
+ var b = epsilon((x: Boolean) => i==i)
+ var b2 = false
+ var n = 0
+ var list: SortedList = Nil()
+ var error = false
+
+ //(while(b) {
+ i = i + 1
+ b = epsilon((x: Boolean) => i==i)
+ b2 = epsilon((x: Boolean) => i==i)
+ n = epsilon((x: Int) => x >= 0)
+ if(b2)
+ list = insert(n, list)
+ else {
+ list = remove(n, list)
+ if(content(list).contains(n))
+ error = true
+ }
+ i = i + 1
+ b = epsilon((x: Boolean) => i==i)
+ b2 = epsilon((x: Boolean) => i==i)
+ n = epsilon((x: Int) => x >= 0)
+ if(b2)
+ list = insert(n, list)
+ else {
+ list = remove(n, list)
+ if(content(list).contains(n))
+ error = true
+ }
+ i = i + 1
+ b = epsilon((x: Boolean) => i==i)
+ b2 = epsilon((x: Boolean) => i==i)
+ n = epsilon((x: Int) => x >= 0)
+ if(b2)
+ list = insert(n, list)
+ else {
+ list = remove(n, list)
+ if(content(list).contains(n))
+ error = true
+ }
+ //}) //invariant(pos(list) && sorted(list, 0))
+ error
+ } ensuring(err => !err) //ensuring(_ == Nil())
+
+}
--
GitLab