Added support for attributes on variable declarations.

1 files changed, 11 insertions, 1 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 75a42200..b3107bcb 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -190,7 +190,7 @@ class AllocatedTests {
   {

     var n := new Node;

     var t := S + {n};

-    

+

     if (*) {

       assert !fresh(n);  // error: n was not allocated in the initial state

     } else {

@@ -498,6 +498,16 @@ class AttributeTests {
   }

 }

 

+// ----------------------- test attributes on variable declarations --------

+

+static method TestAttributesVarDecls()

+{

+  var {:foo} foo;

+  var {:bar} bar := 0;

+  var {:foo} {:bar} foobar := {};

+  var {:baz} baz, {:foobaz} foobaz := true, false;

+}

+

 // ----------------------- Pretty printing of !(!expr) --------

 

 static method TestNotNot()