From 58d639bff25a2d4dadf6febb81b1438e957c43cd Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 15 Jun 2015 16:19:11 -0700
Subject: Do postponsed reads checking also for the body of functions -- see
 Test/dafny0/Reads.dfy for benefits. (Unfortunately, this loses track of the
 "postcondition might not hold on this return path" locations, see
 Test/dafny0/FunctionSpecifications.dfy.)

---
 Test/dafny0/Reads.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index f1c840c3..7e0ca1c4 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -123,6 +123,6 @@ function FunctionInQuantifier2(): int
   requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100
   ensures FunctionInQuantifier2() == 100
 {
-  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // error: insufficient reads for f.reads(10)
+  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // fine :) :)
   f(10)
 }
-- 
cgit v1.2.3