From 6e5fb70941531435489c1dc533d7caea9120a3d5 Mon Sep 17 00:00:00 2001
From: chmaria <unknown>
Date: Sat, 1 Nov 2014 13:59:31 +0100
Subject: Added initial support for dirty while statements.

---
 Test/dafny0/DirtyLoops.dfy        | 17 ++++++++++++++++-
 Test/dafny0/DirtyLoops.dfy.expect |  2 +-
 2 files changed, 17 insertions(+), 2 deletions(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy
index 6a49e733..5d356f0a 100644
--- a/Test/dafny0/DirtyLoops.dfy
+++ b/Test/dafny0/DirtyLoops.dfy
@@ -1,6 +1,21 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method M(S: set<int>) {
+method M0(S: set<int>) {
   forall s | s in S ensures s < 0;
 }
+
+method M1(x: int)
+{
+  var i := x;
+  while (0 < i)
+    invariant i <= x;
+}
+
+method M2(x: int)
+{
+  var i := x;
+  while (0 < i)
+    invariant i <= x;
+    decreases i;
+}
diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect
index 5c12e1ef..060f3287 100644
--- a/Test/dafny0/DirtyLoops.dfy.expect
+++ b/Test/dafny0/DirtyLoops.dfy.expect
@@ -1,4 +1,4 @@
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
 
 Dafny program verifier finished with 0 verified, 0 errors
-- 
cgit v1.2.3