From cb1c7ef8e8b2810e093a5f43531d38c250db59c0 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sun, 27 Mar 2011 18:00:28 +0000
Subject: Dafny: Added support for an initializing call as part of the
 new-allocation syntax.  What you previously would have written like:

  c := new C;
  call c.Init(x, y);

you can now write as:

  c := new C.Init(x, y);
---
 Test/dafny0/Answer | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'Test/dafny0/Answer')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 08570842..f57c6ead 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -79,7 +79,9 @@ TypeTests.dfy(64,6): Error: Duplicate local-variable name: z
 TypeTests.dfy(66,6): Error: Duplicate local-variable name: x
 TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
 TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
-14 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(79,17): Error: member F in class C does not refer to a method
+TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments
+16 resolution/type errors detected in TypeTests.dfy
 
 -------------------- SmallTests.dfy --------------------
 SmallTests.dfy(30,11): Error: index out of range
@@ -142,8 +144,14 @@ Execution trace:
     (0,0): anon6
     (0,0): anon14_Then
     (0,0): anon11
+SmallTests.dfy(272,24): Error BP5002: A precondition for this call might not hold.
+SmallTests.dfy(250,30): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    SmallTests.dfy(267,19): anon3_Else
+    (0,0): anon2
 
-Dafny program verifier finished with 29 verified, 12 errors
+Dafny program verifier finished with 34 verified, 13 errors
 
 -------------------- Definedness.dfy --------------------
 Definedness.dfy(8,7): Error: possible division by zero
-- 
cgit v1.2.3