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

5 files changed, 20 insertions, 20 deletions

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