Refactor resolver, and really allow reads to take fields of type A -> set<obj>

twoState and codeContext is moved to a new class ResolveOpts

2 files changed, 31 insertions, 1 deletions

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)
+  }
+}
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index e83e017c..f1da2003 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -36,4 +36,4 @@ Execution trace:
     ReadsReads.dfy(95,16): anon15_Else

     (0,0): anon21_Then

 

-Dafny program verifier finished with 13 verified, 9 errors

+Dafny program verifier finished with 17 verified, 9 errors