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

13 files changed, 52 insertions, 45 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c4bc6cdd..8bb628a8 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4112,7 +4112,9 @@ namespace Microsoft.Dafny {
                                            * makes reads clauses also guard the requires */

                    , null);

 

-        CheckWellformedWithResult(f.Body, new WFOptions(null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);

+        wfo = new WFOptions(null, true, true /* do delayed reads checks */);

+        CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);

+        wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, bodyCheckBuilder);

       }

       // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch

       postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));

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

diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect
index 6657cd8c..57761ab4 100644
--- a/Test/dafny0/Backticks.dfy.expect
+++ b/Test/dafny0/Backticks.dfy.expect
@@ -1,8 +1,9 @@
 Backticks.dfy(38,5): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

     (0,0): anon7_Else

+    (0,0): anon8_Else

+    (0,0): anon6

 Backticks.dfy(77,8): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect
index 62b67cc3..619a9c84 100644
--- a/Test/dafny0/Corecursion.dfy.expect
+++ b/Test/dafny0/Corecursion.dfy.expect
@@ -13,17 +13,17 @@ Execution trace:
 Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index 6d4bdfbb..9f76313a 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -1,22 +1,24 @@
-FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path.

+FunctionSpecifications.dfy(29,10): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

     (0,0): anon10_Else

-    (0,0): anon11_Then

-    (0,0): anon12_Else

-FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path.

+    (0,0): anon11_Else

+    (0,0): anon12_Then

+    (0,0): anon13_Else

+    (0,0): anon9

+FunctionSpecifications.dfy(38,10): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon14_Else

-    (0,0): anon17_Else

-    (0,0): anon18_Then

+    (0,0): anon15_Else

+    (0,0): anon18_Else

+    (0,0): anon19_Then

+    (0,0): anon14

 FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon10_Then

+    (0,0): anon11_Then

     (0,0): anon5

 FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold.

diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect
index abc253c1..5af90253 100644
--- a/Test/dafny0/NatTypes.dfy.expect
+++ b/Test/dafny0/NatTypes.dfy.expect
@@ -32,9 +32,9 @@ Execution trace:
 NatTypes.dfy(109,45): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

     (0,0): anon8_Else

-    (0,0): anon9_Then

+    (0,0): anon9_Else

+    (0,0): anon10_Then

 NatTypes.dfy(132,35): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/PredExpr.dfy.expect b/Test/dafny0/PredExpr.dfy.expect
index 744b091a..18d5d73f 100644
--- a/Test/dafny0/PredExpr.dfy.expect
+++ b/Test/dafny0/PredExpr.dfy.expect
@@ -5,8 +5,8 @@ Execution trace:
 PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

     (0,0): anon7_Else

+    (0,0): anon8_Else

 PredExpr.dfy(52,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/RankNeg.dfy.expect b/Test/dafny0/RankNeg.dfy.expect
index cf077cc4..b2686b43 100644
--- a/Test/dafny0/RankNeg.dfy.expect
+++ b/Test/dafny0/RankNeg.dfy.expect
@@ -1,22 +1,22 @@
 RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 

 Dafny program verifier finished with 1 verified, 4 errors

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index f1c840c3..7e0ca1c4 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -123,6 +123,6 @@ function FunctionInQuantifier2(): int
   requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100
   ensures FunctionInQuantifier2() == 100
 {
-  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // error: insufficient reads for f.reads(10)
+  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // fine :) :)
   f(10)
 }
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 79d290da..0b599f3f 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -31,9 +31,5 @@ Execution trace:
 Reads.dfy(120,38): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-Reads.dfy(126,26): Error: insufficient reads clause to invoke function

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Else

 

-Dafny program verifier finished with 15 verified, 10 errors

+Dafny program verifier finished with 16 verified, 9 errors

diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index bc59c722..77a9e70e 100644
--- a/Test/dafny0/Termination.dfy.expect
+++ b/Test/dafny0/Termination.dfy.expect
@@ -4,9 +4,9 @@ Execution trace:
 Termination.dfy(361,47): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Else

-    (0,0): anon9_Then

-    (0,0): anon10_Else

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+    (0,0): anon11_Else

 Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

@@ -44,9 +44,9 @@ Execution trace:
 Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

     (0,0): anon8_Else

-    (0,0): anon9_Then

+    (0,0): anon9_Else

+    (0,0): anon10_Then

 Termination.dfy(296,3): Error: decreases expression might not decrease

 Execution trace:

     Termination.dfy(296,3): anon9_LoopHead

diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect
index 880dcc47..21188d62 100644
--- a/Test/hofs/Classes.dfy.expect
+++ b/Test/hofs/Classes.dfy.expect
@@ -1,10 +1,10 @@
 Classes.dfy(41,6): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Then

-    (0,0): anon4

     (0,0): anon13_Then

-    (0,0): anon14_Else

+    (0,0): anon4

+    (0,0): anon14_Then

     (0,0): anon15_Else

+    (0,0): anon16_Else

 

 Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
index a38dc560..b4dfc561 100644
--- a/Test/hofs/Naked.dfy.expect
+++ b/Test/hofs/Naked.dfy.expect
@@ -1,20 +1,20 @@
 Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Else

     (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

+    (0,0): anon11_Then

 Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Else

     (0,0): anon9_Else

     (0,0): anon10_Else

+    (0,0): anon11_Else

 Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

     (0,0): anon7_Else

+    (0,0): anon8_Else

 Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0