From 58d639bff25a2d4dadf6febb81b1438e957c43cd Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 15 Jun 2015 16:19:11 -0700
Subject: 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.)

---
 Test/hofs/Classes.dfy.expect | 6 +++---
 Test/hofs/Naked.dfy.expect   | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'Test/hofs')

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