Dafny: Extended the support for attributes on method/constructor calls.

1 files changed, 16 insertions, 5 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index e6590ed1..5fabe354 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -438,7 +438,7 @@ class AttributeTests {
 

   }

 

-  method testAttributes0()

+  method testAttributes0() returns (r: AttributeTests)

     ensures {:boolAttr true} true;

     ensures {:boolAttr false} true;

     ensures {:intAttr 0} true;

@@ -491,19 +491,30 @@ class AttributeTests {
     m0() {:intAttr 0};

     m0() {:intAttr 1};

 

+    this.m0() {:boolAttr true};

+    this.m0() {:boolAttr false};

+    this.m0() {:intAttr 0};

+    this.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 b2, b2' := m2() {:boolAttr true}, m2() {:boolAttr true};

+    b2, b2' := m2() {:boolAttr false}, m2() {:boolAttr false};

+    b2, b2' := m2() {:intAttr 0}, m2() {:boolAttr false};

+    b2, b2' := m2() {:intAttr 1}, m2() {:boolAttr false};

 

     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};

+

+    if (*) {

+      return new AttributeTests.C() {:boolAttr true};

+    } else {

+      return new AttributeTests.C() {:intAttr 0};

+    }

   }

 }