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.)

1 files changed, 6 insertions, 0 deletions

diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect
index ff05137b..59dcb4bf 100644
--- a/Test/dafny0/Array.dfy.expect
+++ b/Test/dafny0/Array.dfy.expect
@@ -48,6 +48,7 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon12_Then

     (0,0): anon13_Then

+    (0,0): anon9

 Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

     (0,0): anon0

@@ -55,6 +56,7 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon12_Then

     (0,0): anon13_Else

+    (0,0): anon9

 Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

     (0,0): anon0

@@ -62,6 +64,7 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon12_Then

     (0,0): anon13_Else

+    (0,0): anon9

 Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

     (0,0): anon0

@@ -69,18 +72,21 @@ Execution trace:
     (0,0): anon11_Then

     (0,0): anon12_Then

     (0,0): anon13_Else

+    (0,0): anon9

 Array.dfy(163,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Else

     (0,0): anon9_Then

     (0,0): anon10_Then

+    (0,0): anon7

 Array.dfy(171,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Else

     (0,0): anon9_Then

     (0,0): anon10_Then

+    (0,0): anon7

 Array.dfy(187,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0