Postpone reads checks of function preconditions until after the entire precondition has otherwise been checked for well-formedness

31 files changed, 170 insertions, 165 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e93e91df..c4bc6cdd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4021,6 +4021,7 @@ namespace Microsoft.Dafny {
       var implInParams = Bpl.Formal.StripWhereClauses(inParams);

       var locals = new List<Variable>();

       var builder = new Bpl.StmtListBuilder();

+      var builderInitializationArea = new Bpl.StmtListBuilder();

       builder.Add(new CommentCmd("AddWellformednessCheck for function " + f));

       builder.Add(CaptureState(f.tok, false, "initial state"));

 

@@ -4028,19 +4029,17 @@ namespace Microsoft.Dafny {
 

       // check well-formedness of the preconditions (including termination, and reads checks), and then

       // assume each one of them

-      var wfo = new WFOptions(null, true, true /* do delayed reads checks over requires */);

 

       // check well-formedness of the reads clause

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

       CheckFrameWellFormed(wfo, f.Reads, locals, builder, etran);

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

 

-      // check the reads of the preconditions now

-      foreach (var a in wfo.Asserts) {

-        builder.Add(a);

-      }

-

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

       foreach (Expression p in f.Req) {

-        CheckWellformedAndAssume(p, new WFOptions(null, true /* do reads checks */), locals, builder, etran);

+        CheckWellformedAndAssume(p, wfo, locals, builder, etran);

       }

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

 

       // check well-formedness of the decreases clauses (including termination, but no reads checks)

       foreach (Expression p in f.Decreases.Expressions)

@@ -4119,16 +4118,12 @@ namespace Microsoft.Dafny {
       postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));

       builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok)));

 

-      // var b$reads_guards_requires#0 : bool

-      locals.AddRange(wfo.Locals);

-      // This ugly way seems to be the way to add things at the start of a builder:

-      StmtList sl = builder.Collect(f.tok);

-      // b$reads_guards_requires#0 := true   ...

-      sl.BigBlocks[0].simpleCmds.InsertRange(0, wfo.AssignLocals);

-

+      var s0 = builderInitializationArea.Collect(f.tok);

+      var s1 = builder.Collect(f.tok);

+      var implBody = new StmtList(new List<BigBlock>(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok);

       Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name,

         typeParams, Concat(typeInParams, implInParams), new List<Variable>(),

-        locals, sl, etran.TrAttributes(f.Attributes, null));

+        locals, implBody, etran.TrAttributes(f.Attributes, null));

       sink.AddTopLevelDeclaration(impl);

 

       if (InsertChecksums)

@@ -4582,7 +4577,11 @@ namespace Microsoft.Dafny {
     /// like it.  This is useful in function postconditions, where the result of the function is

     /// syntactically given as what looks like a recursive call with the same arguments.

     /// "DoReadsChecks" indicates whether or not to perform reads checks.  If so, the generated code

-    /// will make references to $_Frame.

+    /// will make references to $_Frame.  If "saveReadsChecks" is true, then the reads checks will

+    /// be recorded but postponsed.  In particular, CheckWellformed will append to .Locals a list of

+    /// fresh local variables and will append to .Assert assertions with appropriate error messages

+    /// that can be used later.  As a convenience, the ProcessSavedReadsChecks will make use of .Locals

+    /// and .Asserts (and AssignLocals) and update a given StmtListBuilder.

     /// </summary>

     private class WFOptions

     {

@@ -4596,6 +4595,7 @@ namespace Microsoft.Dafny {
       }

 

       public WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool saveReadsChecks = false) {

+        Contract.Requires(!saveReadsChecks || doReadsChecks);  // i.e., saveReadsChecks ==> doReadsChecks

         SelfCallsAllowance = selfCallsAllowance;

         DoReadsChecks = doReadsChecks;

         if (saveReadsChecks) {

@@ -4629,6 +4629,24 @@ namespace Microsoft.Dafny {
             );

         }

       }

+

+      public void ProcessSavedReadsChecks(List<Variable> locals, StmtListBuilder builderInitializationArea, StmtListBuilder builder) {

+        Contract.Requires(locals != null);

+        Contract.Requires(builderInitializationArea != null);

+        Contract.Requires(builder != null);

+        Contract.Requires(Locals != null && Asserts != null);  // ProcessSavedReadsChecks should be called only if the constructor was called with saveReadsChecks

+

+        // var b$reads_guards#0 : bool  ...

+        locals.AddRange(Locals);

+        // b$reads_guards#0 := true   ...

+        foreach (var cmd in AssignLocals) {

+          builderInitializationArea.Add(cmd);

+        }

+        // assert b$reads_guards#0;  ...

+        foreach (var a in Asserts) {

+          builder.Add(a);

+        }

+      }

     }

 

     void TrStmt_CheckWellformed(Expression expr, Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran, bool subsumption) {

@@ -4636,6 +4654,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

 

       Bpl.QKeyValue kv;

       if (subsumption) {

@@ -4738,10 +4757,13 @@ namespace Microsoft.Dafny {
         return;

       }

       // resort to the behavior of simply checking well-formedness followed by assuming the translated expression

-      CheckWellformedWithResult(expr, options, null, null, locals, builder, etran);

+      CheckWellformed(expr, options, locals, builder, etran);

       builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));

     }

 

+    /// <summary>

+    /// Check the well-formedness of "expr" (but don't leave hanging around any assumptions that affect control flow)

+    /// </summary>

     void CheckWellformed(Expression expr, WFOptions options, List<Variable> locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {

       Contract.Requires(expr != null);

       Contract.Requires(options != null);

@@ -5292,21 +5314,9 @@ namespace Microsoft.Dafny {
 

             // Check frame WF and that it read covers itself

             newOptions = new WFOptions(options.SelfCallsAllowance, true /* check reads clauses */, true /* delay reads checks */);

-

             CheckFrameWellFormed(newOptions, reads, locals, newBuilder, newEtran);

-

             // new options now contains the delayed reads checks

-            locals.AddRange(newOptions.Locals);

-            // assign locals to true, but at a scope above

-            Contract.Assert(newBuilder != builder);

-            foreach (var a in newOptions.AssignLocals) {

-              builder.Add(a);

-            }

-

-            // add asserts to the current builder (right after frame WF)

-            foreach (var a in newOptions.Asserts) {

-              newBuilder.Add(a);

-            }

+            newOptions.ProcessSavedReadsChecks(locals, builder, newBuilder);

 

             // continue doing reads checks, but don't delay them

             newOptions = new WFOptions(options.SelfCallsAllowance, true, false);

diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect
index bf4da25f..ff05137b 100644
--- a/Test/dafny0/Array.dfy.expect
+++ b/Test/dafny0/Array.dfy.expect
@@ -44,43 +44,43 @@ Execution trace:
 Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

     (0,0): anon11_Then

     (0,0): anon12_Then

+    (0,0): anon13_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

     (0,0): anon11_Then

-    (0,0): anon12_Else

+    (0,0): anon12_Then

+    (0,0): anon13_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

     (0,0): anon11_Then

-    (0,0): anon12_Else

+    (0,0): anon12_Then

+    (0,0): anon13_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

     (0,0): anon11_Then

-    (0,0): anon12_Else

+    (0,0): anon12_Then

+    (0,0): anon13_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Then

+    (0,0): anon8_Else

     (0,0): anon9_Then

+    (0,0): anon10_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Then

+    (0,0): anon8_Else

     (0,0): anon9_Then

+    (0,0): anon10_Then

 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/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect
index 547b676d..8486716d 100644
--- a/Test/dafny0/AutoReq.dfy.expect
+++ b/Test/dafny0/AutoReq.dfy.expect
@@ -2,17 +2,17 @@ AutoReq.dfy(247,5): Error: possible violation of function precondition
 AutoReq.dfy(239,14): Related location

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 AutoReq.dfy(13,3): Error: possible violation of function precondition

 AutoReq.dfy(5,14): Related location

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 AutoReq.dfy(25,3): Error: possible violation of function precondition

 AutoReq.dfy(5,14): Related location

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 AutoReq.dfy(38,12): Error: assertion violation

 AutoReq.dfy(31,13): Related location

 AutoReq.dfy(7,5): Related location

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

     (0,0): anon6_Else

+    (0,0): anon7_Else

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

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/BadFunction.dfy.expect b/Test/dafny0/BadFunction.dfy.expect
index 7127b60b..9c4ae81d 100644
--- a/Test/dafny0/BadFunction.dfy.expect
+++ b/Test/dafny0/BadFunction.dfy.expect
@@ -1,6 +1,6 @@
 BadFunction.dfy(9,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 

 Dafny program verifier finished with 2 verified, 1 error

diff --git a/Test/dafny0/ComputationsLoop.dfy.expect b/Test/dafny0/ComputationsLoop.dfy.expect
index d9d48024..91dc2af9 100644
--- a/Test/dafny0/ComputationsLoop.dfy.expect
+++ b/Test/dafny0/ComputationsLoop.dfy.expect
@@ -1,7 +1,7 @@
 ComputationsLoop.dfy(7,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ComputationsLoop.dfy(12,26): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/ComputationsLoop2.dfy.expect b/Test/dafny0/ComputationsLoop2.dfy.expect
index 0a45e6d0..816cbd31 100644
--- a/Test/dafny0/ComputationsLoop2.dfy.expect
+++ b/Test/dafny0/ComputationsLoop2.dfy.expect
@@ -1,11 +1,11 @@
 ComputationsLoop2.dfy(6,3): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ComputationsLoop2.dfy(16,26): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/ComputationsNeg.dfy.expect b/Test/dafny0/ComputationsNeg.dfy.expect
index 16c8963f..a6318087 100644
--- a/Test/dafny0/ComputationsNeg.dfy.expect
+++ b/Test/dafny0/ComputationsNeg.dfy.expect
@@ -1,7 +1,7 @@
 ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path.

 ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold.

 Execution trace:

diff --git a/Test/dafny0/ControlStructures.dfy.expect b/Test/dafny0/ControlStructures.dfy.expect
index 43124912..3f4dce92 100644
--- a/Test/dafny0/ControlStructures.dfy.expect
+++ b/Test/dafny0/ControlStructures.dfy.expect
@@ -26,11 +26,11 @@ Execution trace:
 ControlStructures.dfy(54,3): Error: missing case in case statement: Red

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Else

     (0,0): anon9_Else

     (0,0): anon10_Else

     (0,0): anon11_Else

-    (0,0): anon12_Then

+    (0,0): anon12_Else

+    (0,0): anon13_Then

 ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect
index e30f6f1a..62b67cc3 100644
--- a/Test/dafny0/Corecursion.dfy.expect
+++ b/Test/dafny0/Corecursion.dfy.expect
@@ -1,36 +1,36 @@
 Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 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): anon5_Else

+    (0,0): anon6_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): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_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): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_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

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Corecursion.dfy(161,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

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 

 Dafny program verifier finished with 20 verified, 8 errors

diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect
index 874df45e..4c0b1e96 100644
--- a/Test/dafny0/Datatypes.dfy.expect
+++ b/Test/dafny0/Datatypes.dfy.expect
@@ -16,27 +16,27 @@ Execution trace:
 Datatypes.dfy(349,5): Error: missing case in case statement: Cons

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon7_Then

+    (0,0): anon7_Else

+    (0,0): anon8_Then

 Datatypes.dfy(349,5): Error: missing case in case statement: Nil

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

     (0,0): anon7_Else

-    (0,0): anon8_Then

+    (0,0): anon8_Else

+    (0,0): anon9_Then

 Datatypes.dfy(356,8): Error: missing case in case statement: Cons

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

     (0,0): anon11_Then

+    (0,0): anon12_Then

 Datatypes.dfy(356,8): Error: missing case in case statement: Nil

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_Else

-    (0,0): anon12_Then

+    (0,0): anon10_Else

+    (0,0): anon11_Then

+    (0,0): anon12_Else

+    (0,0): anon13_Then

 Datatypes.dfy(82,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect
index 5d823616..af5b62b9 100644
--- a/Test/dafny0/Definedness.dfy.expect
+++ b/Test/dafny0/Definedness.dfy.expect
@@ -1,7 +1,7 @@
 Definedness.dfy(11,7): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Definedness.dfy(18,16): Error: possible division by zero

 Execution trace:

     (0,0): anon0

@@ -161,15 +161,15 @@ Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this re
 Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Definedness.dfy(224,22): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

+    (0,0): anon4_Then

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

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 

 Dafny program verifier finished with 21 verified, 37 errors

diff --git a/Test/dafny0/DeterministicPick.dfy.expect b/Test/dafny0/DeterministicPick.dfy.expect
index f8b779ef..0999294e 100644
--- a/Test/dafny0/DeterministicPick.dfy.expect
+++ b/Test/dafny0/DeterministicPick.dfy.expect
@@ -1,6 +1,6 @@
 DeterministicPick.dfy(13,5): Error: to be compilable, the value of a let-such-that expression must be uniquely determined

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 

 Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index f5112bfe..6d4bdfbb 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -2,27 +2,27 @@ FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold
 FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Else

     (0,0): anon9_Else

-    (0,0): anon10_Then

-    (0,0): anon11_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.

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon13_Else

-    (0,0): anon16_Else

-    (0,0): anon17_Then

+    (0,0): anon14_Else

+    (0,0): anon17_Else

+    (0,0): anon18_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon4

+    (0,0): anon10_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.

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 FunctionSpecifications.dfy(108,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -40,28 +40,28 @@ Execution trace:
 FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 FunctionSpecifications.dfy(153,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Include.dfy.expect b/Test/dafny0/Include.dfy.expect
index cb329398..0921cec9 100644
--- a/Test/dafny0/Include.dfy.expect
+++ b/Test/dafny0/Include.dfy.expect
@@ -2,7 +2,7 @@ Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return
 Includee.dfy(17,20): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Includee.dfy[Concrete](22,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect
index c6df95b8..66dc2764 100644
--- a/Test/dafny0/LetExpr.dfy.expect
+++ b/Test/dafny0/LetExpr.dfy.expect
@@ -24,11 +24,11 @@ Execution trace:
 LetExpr.dfy(305,42): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 LetExpr.dfy(307,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 LetExpr.dfy(317,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect
index 99fa16e5..abc253c1 100644
--- a/Test/dafny0/NatTypes.dfy.expect
+++ b/Test/dafny0/NatTypes.dfy.expect
@@ -32,12 +32,12 @@ Execution trace:
 NatTypes.dfy(109,45): 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_Then

+    (0,0): anon8_Else

+    (0,0): anon9_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

+    (0,0): anon4_Then

 

 Dafny program verifier finished with 15 verified, 9 errors

diff --git a/Test/dafny0/PredExpr.dfy.expect b/Test/dafny0/PredExpr.dfy.expect
index 07bd5f20..744b091a 100644
--- a/Test/dafny0/PredExpr.dfy.expect
+++ b/Test/dafny0/PredExpr.dfy.expect
@@ -1,12 +1,12 @@
 PredExpr.dfy(7,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

     (0,0): anon6_Else

+    (0,0): anon7_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 d740f8a0..cf077cc4 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): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

 

 Dafny program verifier finished with 1 verified, 4 errors

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 6ae07d53..545c9a18 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -72,7 +72,7 @@ class CircularChecking {
 
   function G1(): int
     reads this
-    requires F() == 100  // error: it is not known (yet) that the rest of what F() reads (namely, Repr) is empty
+    requires F() == 100  // fine, since the next line tells us that Repr is empty
     requires Repr == {}
 
   function H0(cell: Cell): int
@@ -86,7 +86,7 @@ class CircularChecking {
 
   function H2(cell: Cell): int
     reads this, Repr
-    requires cell != null && cell.data == 10  // error: it is not known (yet) that "cell in Repr"
+    requires cell != null && cell.data == 10  // this is okay, too, since reads checks are postponed
     requires cell in Repr
 }
 
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 0b6a2d5a..9873f811 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -1,31 +1,26 @@
-Reads.dfy(75,14): Error: insufficient reads clause to invoke function

-Execution trace:

-    (0,0): anon0

 Reads.dfy(79,11): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-Reads.dfy(89,35): Error: insufficient reads clause to read field

-Execution trace:

-    (0,0): anon0

 Reads.dfy(9,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

 Reads.dfy(18,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon3

+    (0,0): anon10_Then

+    (0,0): anon4

 Reads.dfy(28,50): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

 Reads.dfy(37,43): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Then

+    (0,0): anon7_Then

+    (0,0): anon4

 Reads.dfy(51,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon3

+    (0,0): anon10_Then

+    (0,0): anon4

 

-Dafny program verifier finished with 9 verified, 8 errors

+Dafny program verifier finished with 11 verified, 6 errors

diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect
index 93d59873..d03b9412 100644
--- a/Test/dafny0/Refinement.dfy.expect
+++ b/Test/dafny0/Refinement.dfy.expect
@@ -16,7 +16,7 @@ Refinement.dfy(99,12): Error BP5003: A postcondition might not hold on this retu
 Refinement.dfy(78,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Refinement.dfy(102,3): Error BP5003: A postcondition might not hold on this return path.

 Refinement.dfy(83,15): Related location: This is the postcondition that might not hold.

 Execution trace:

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index b475502a..3df8118a 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -4,18 +4,18 @@ Execution trace:
 SmallTests.dfy(65,36): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Then

+    (0,0): anon13_Then

 SmallTests.dfy(66,51): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Else

     (0,0): anon13_Else

+    (0,0): anon14_Else

 SmallTests.dfy(67,22): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    (0,0): anon12_Then

     (0,0): anon13_Then

     (0,0): anon14_Then

+    (0,0): anon15_Then

 SmallTests.dfy(86,24): Error: target object may be null

 Execution trace:

     (0,0): anon0

@@ -91,7 +91,7 @@ Execution trace:
 SmallTests.dfy(386,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 SmallTests.dfy(691,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -125,12 +125,12 @@ Execution trace:
 SmallTests.dfy(354,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 SmallTests.dfy(401,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 SmallTests.dfy(562,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/StatementExpressions.dfy.expect b/Test/dafny0/StatementExpressions.dfy.expect
index 313c8884..9de6a5d1 100644
--- a/Test/dafny0/StatementExpressions.dfy.expect
+++ b/Test/dafny0/StatementExpressions.dfy.expect
@@ -11,11 +11,11 @@ Execution trace:
 StatementExpressions.dfy(77,6): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 StatementExpressions.dfy(98,18): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
index eccb16b0..6497c712 100644
--- a/Test/dafny0/Superposition.dfy.expect
+++ b/Test/dafny0/Superposition.dfy.expect
@@ -14,7 +14,7 @@ Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 

 Verifying CheckWellformed$$_0_M0.C.R ...

   [5 proof obligations]  error

@@ -22,7 +22,7 @@ Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Else

+    (0,0): anon7_Else

 

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

@@ -36,9 +36,9 @@ Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Else

-    (0,0): anon10_Then

-    (0,0): anon7

+    (0,0): anon9_Else

+    (0,0): anon11_Then

+    (0,0): anon8

 

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index 98aa0cd8..bc59c722 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): anon7_Else

-    (0,0): anon8_Then

-    (0,0): anon9_Else

+    (0,0): anon8_Else

+    (0,0): anon9_Then

+    (0,0): anon10_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): anon6_Else

     (0,0): anon7_Else

-    (0,0): anon8_Then

+    (0,0): anon8_Else

+    (0,0): anon9_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 3c933bae..880dcc47 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): anon11_Then

-    (0,0): anon3

     (0,0): anon12_Then

-    (0,0): anon13_Else

+    (0,0): anon4

+    (0,0): anon13_Then

     (0,0): anon14_Else

+    (0,0): anon15_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 62c035b2..a38dc560 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): anon7_Else

     (0,0): anon8_Else

-    (0,0): anon9_Then

+    (0,0): anon9_Else

+    (0,0): anon10_Then

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

     (0,0): anon8_Else

     (0,0): anon9_Else

+    (0,0): anon10_Else

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

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

     (0,0): anon6_Else

+    (0,0): anon7_Else

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

 Execution trace:

     (0,0): anon0

@@ -24,12 +24,12 @@ Execution trace:
 Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Naked.dfy(29,30): Error: possible violation of function precondition

 Naked.dfy(32,14): Related location

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 Execution trace:

     (0,0): anon0

@@ -42,7 +42,7 @@ Execution trace:
 Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

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

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index 73002b73..cd013630 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -1,19 +1,19 @@
 ReadsReads.dfy(31,7): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(36,5): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(47,12): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(87,50): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index b3c126d5..1a1027ae 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -1,13 +1,13 @@
 Simple.dfy(14,10): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

 Simple.dfy(27,10): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

 Simple.dfy(37,9): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect
index 5ba4b47b..2476b945 100644
--- a/Test/hofs/Twice.dfy.expect
+++ b/Test/hofs/Twice.dfy.expect
@@ -5,7 +5,7 @@ Execution trace:
 Twice.dfy(35,32): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

+    (0,0): anon11_Then

 

 Dafny program verifier finished with 4 verified, 2 errors