From 2ef4d9e637e0633347c4030b50925a92f8c12963 Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Fri, 15 Aug 2014 11:46:59 -0700
Subject: Refactor resolver, and really allow reads to take fields of type A ->
 set<obj>

twoState and codeContext is moved to a new class ResolveOpts
---
 Test/hofs/ReadsReads.dfy | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

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

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index 47f7f575..d0a8b43b 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -101,3 +101,33 @@ module WhatWeKnowAboutReads {
     }
   }
 }
+
+module ReadsAll {
+  function A(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method B(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function C(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method D(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+}
-- 
cgit v1.2.3