From d92e95d5fb8afdcf8f8dca77e541ad3032bfdff4 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 1 May 2015 14:02:27 -0700
Subject: Improved encoding of a property of reads clauses to make things more
 easily provable.

---
 Test/hofs/ReadsReads.dfy | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'Test/hofs')

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index d0a8b43b..3fb03fda 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -131,3 +131,14 @@ module ReadsAll {
     f(0) + f(1) + f(2)
   }
 }
+
+module ReadsOnFunctions {
+  lemma M0(f: int -> int)
+  {
+    var g := f.requires;
+    assert g.reads(10) == f.reads(10);
+  }
+//  function F(f: int -> int): int
+//    requires forall x :: f.reads(x) == {}  // should always be allowed to invoke .reads, even if F has an empty reads clause
+//  { 0 }
+}
-- 
cgit v1.2.3