From 2edb5e1ba0f8c9c79364d0f0415713f0ddfdeadd Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 15 Jun 2015 15:04:18 -0700
Subject: Postpone reads checks of function preconditions until after the
 entire precondition has otherwise been checked for well-formedness

---
 Test/hofs/Classes.dfy.expect    |  6 +++---
 Test/hofs/Naked.dfy.expect      | 14 +++++++-------
 Test/hofs/ReadsReads.dfy.expect |  8 ++++----
 Test/hofs/Simple.dfy.expect     |  8 ++++----
 Test/hofs/Twice.dfy.expect      |  4 ++--
 5 files changed, 20 insertions(+), 20 deletions(-)

(limited to 'Test/hofs')

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
-- 
cgit v1.2.3