diff options
Diffstat (limited to 'Test/dafny4')
-rw-r--r-- | Test/dafny4/Bug136.dfy | 12 | ||||
-rw-r--r-- | Test/dafny4/Bug136.dfy.expect | 2 | ||||
-rw-r--r-- | Test/dafny4/Bug138.dfy | 22 | ||||
-rw-r--r-- | Test/dafny4/Bug138.dfy.expect | 2 | ||||
-rw-r--r-- | Test/dafny4/Bug140.dfy | 67 | ||||
-rw-r--r-- | Test/dafny4/Bug140.dfy.expect | 6 |
6 files changed, 111 insertions, 0 deletions
diff --git a/Test/dafny4/Bug136.dfy b/Test/dafny4/Bug136.dfy new file mode 100644 index 00000000..97c9e389 --- /dev/null +++ b/Test/dafny4/Bug136.dfy @@ -0,0 +1,12 @@ +// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method test()
+{
+ assume false;
+ assert true;
+}
+
+
+
+
diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny4/Bug136.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny4/Bug138.dfy b/Test/dafny4/Bug138.dfy new file mode 100644 index 00000000..db0e54ef --- /dev/null +++ b/Test/dafny4/Bug138.dfy @@ -0,0 +1,22 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype List = Nil | Cons(int, List)
+
+method R(xs: List)
+{
+ match xs
+ case Nil() => // currently produces a parsing error, but shouldn't
+ case Cons(x, Nil()) => // currently allowed
+ case Cons(x, Cons(y, tail)) =>
+}
+
+function F(xs: List) : int
+{
+ match xs
+ case Nil() => 0 // currently produces a parsing error, but shouldn't
+ case Cons(x, Nil()) => 1 // currently allowed
+ case Cons(x, Cons(y, tail)) => 2
+}
+
+
diff --git a/Test/dafny4/Bug138.dfy.expect b/Test/dafny4/Bug138.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug138.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny4/Bug140.dfy b/Test/dafny4/Bug140.dfy new file mode 100644 index 00000000..9a85e36c --- /dev/null +++ b/Test/dafny4/Bug140.dfy @@ -0,0 +1,67 @@ +// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t" + +class Node<T> { + ghost var List: seq<T>; + ghost var Repr: set<Node<T>>; + + var data: T; + var next: Node<T>; + + predicate Valid() + reads this, Repr + { + this in Repr && null !in Repr && + (next == null ==> List == [data]) && + (next != null ==> + next in Repr && next.Repr <= Repr && + this !in next.Repr && + List == [data] + next.List && + next.Valid()) + } + + constructor (d: T) + modifies this + ensures Valid() && fresh(Repr - {this}) + ensures List == [d] + { + data, next := d, null; + List, Repr := [d], {this}; + } + + constructor InitAsPredecessor(d: T, succ: Node<T>) + requires succ != null && succ.Valid() && this !in succ.Repr; + modifies this; + ensures Valid() && fresh(Repr - {this} - succ.Repr); + ensures List == [d] + succ.List; + { + data, next := d, succ; + List := [d] + succ.List; + Repr := {this} + succ.Repr; + } + + method Prepend(d: T) returns (r: Node<T>) + requires Valid() + ensures r != null && r.Valid() && fresh(r.Repr - old(Repr)) + ensures r.List == [d] + List + { + r := new Node.InitAsPredecessor(d, this); + } + + method Print() + requires Valid() + decreases |List| + { + print data; + if (next != null) { + next.Print(); + } + } +} + +method Main() +{ + var l2 := new Node(2); + var l1 := l2.Prepend(1); + l1.Print(); +} diff --git a/Test/dafny4/Bug140.dfy.expect b/Test/dafny4/Bug140.dfy.expect new file mode 100644 index 00000000..00c7d129 --- /dev/null +++ b/Test/dafny4/Bug140.dfy.expect @@ -0,0 +1,6 @@ +
+Dafny program verifier finished with 11 verified, 0 errors
+Program compiled successfully
+Running...
+
+12
\ No newline at end of file |