From 9152bf2ff98b1dce60a347afa4ec39bc3df86c4a Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 21 Dec 2011 17:49:31 +0100
Subject: Dafny: Added support for attributes on method/constructor calls.

---
 Test/dafny0/Answer         |  2 +-
 Test/dafny0/SmallTests.dfy | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index aa58ac6e..5e1428c2 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -247,7 +247,7 @@ SmallTests.dfy(411,41): Error: possible violation of function postcondition
 Execution trace:
     (0,0): anon6_Else
 
-Dafny program verifier finished with 49 verified, 21 errors
+Dafny program verifier finished with 56 verified, 21 errors
 
 -------------------- Definedness.dfy --------------------
 Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 7adc26a3..e6590ed1 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -418,6 +418,26 @@ function F(b: bool): int
 class AttributeTests {
   var f: int;
 
+  method m0()
+  {
+
+  }
+
+  method m1() returns (r: bool)
+  {
+    r := false;
+  }
+
+  function method m2() : bool
+  {
+    true
+  }
+
+  constructor C()
+  {
+
+  }
+
   method testAttributes0()
     ensures {:boolAttr true} true;
     ensures {:boolAttr false} true;
@@ -465,5 +485,25 @@ class AttributeTests {
     {
 
     }
+
+    m0() {:boolAttr true};
+    m0() {:boolAttr false};
+    m0() {:intAttr 0};
+    m0() {:intAttr 1};
+
+    var b1 := m1() {:boolAttr true};
+    b1 := m1() {:boolAttr false};
+    b1 := m1() {:intAttr 0};
+    b1 := m1() {:intAttr 1};
+
+    var b2 := m2() {:boolAttr true};
+    b2 := m2() {:boolAttr false};
+    b2 := m2() {:intAttr 0};
+    b2 := m2() {:intAttr 1};
+
+    var c := new AttributeTests.C() {:boolAttr true};
+    c := new AttributeTests.C() {:boolAttr false};
+    c := new AttributeTests.C() {:intAttr 0};
+    c := new AttributeTests.C() {:intAttr 1};
   }
 }
-- 
cgit v1.2.3