From 9a714cafa2e4d6551f28c57187c28333cc155527 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 27 May 2011 01:19:41 -0700
Subject: Dafny: retired "use" statements

---
 Test/dafny0/Definedness.dfy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/dafny0/Definedness.dfy')

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 255b38e3..92ac0793 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -180,12 +180,12 @@ class StatementTwoShoes {
   method V(s: set<StatementTwoShoes>, a: int, b: int)
     modifies s;
   {
-    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements
+
     foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null
     {
       assume 0 <= m.x;
       assert m.x < 1000;
-      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements
+
       m.x := m.x + 1;
     }
     foreach (m in s + {F(a)})  // error: collection expression may not be well defined (fn precondition)
-- 
cgit v1.2.3