From 8a869bcfaeceb6b5a1d01e9b1c0c08b7000a094e Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 22:47:35 -0700 Subject: Removed specContextOnly parameter from ResolveStatement. Moved all bounds discovery to resolution pass 1. --- Test/hofs/ReadsReads.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/hofs') diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index a6f8d922..60ac35f5 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -105,14 +105,14 @@ module WhatWeKnowAboutReads { module ReadsAll { function A(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o + reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal) 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 + reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal) requires forall x :: f.requires(x) { f(0) + f(1) + f(2) -- cgit v1.2.3