From 1f38d2d252aaac3d55191e6c3dad46ecffdfee2c Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 1 Mar 2016 15:37:54 -0800
Subject: Revised the $Is and $IsAlloc axioms for arrow terms.  It is now
 possible to derived these predicates.  More things can now be verified
 (including the problem reported in Issue #49).

---
 Test/hofs/OneShot.dfy | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'Test/hofs/OneShot.dfy')

diff --git a/Test/hofs/OneShot.dfy b/Test/hofs/OneShot.dfy
index 286be898..e920530a 100644
--- a/Test/hofs/OneShot.dfy
+++ b/Test/hofs/OneShot.dfy
@@ -10,16 +10,15 @@ method OneShot() {
   var i : Ref<int>;
   i := new Ref;
 
-  g := () -> true;
-
+  g := () reads i -> true;  // using a (deprecated) one-shot arrow here means "g" acquires
+                           // a precondition that says it can only be applied in this heap
   assert g();
 
   i.val := i.val + 1; // heap changes
 
   if * {
-    assert g();         // should fail
+    assert g();         // error: precondition violation
   } else {
-    assert !g();        // should fail
+    assert !g();        // error: precondition violation
   }
 }
-
-- 
cgit v1.2.3