Dafny: Added support for attributes on methods and constructors.

2 files changed, 48 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index f00bb9a0..0c2e487a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -192,6 +192,12 @@ Execution trace:
     (0,0): anon0

     SmallTests.dfy(266,19): anon3_Else

     (0,0): anon2

+SmallTests.dfy(366,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(376,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.

 SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -207,8 +213,11 @@ Execution trace:
     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

+SmallTests.dfy(354,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 44 verified, 15 errors

+Dafny program verifier finished with 47 verified, 18 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 8393b1c7..439930b5 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -8,7 +8,7 @@ class Node {
     (next != null  ==>  next.IsList(r - {this}))

   }

 

-  method Test(n: Node, nodes: set<Node>) 

+  method Test(n: Node, nodes: set<Node>)

   {

     assume nodes == nodes - {n};

     // the next line needs the Set extensionality axiom, the antecedent of

@@ -189,7 +189,7 @@ class AllocatedTests {
   method M(r: AllocatedTests, k: Node, S: set<Node>, d: Lindgren)

   {

     assert allocated(r);

-    

+

     var n := new Node;

     var t := S + {n};

     assert allocated(t);

@@ -346,3 +346,39 @@ method TestSequences0()
   }

   assert 7 in s;  // error

 }

+

+// ----------------------- test attributes on methods and constructors --------

+

+method test0()

+{

+  assert false;  // error

+}

+

+method {:verify false} test1()

+{

+  assert false;

+}

+

+class Test {

+

+  method test0()

+  {

+    assert false;  // error

+  }

+

+  method {:verify false} test1()

+  {

+    assert false;

+  }

+

+  constructor init0()

+  {

+    assert false;  // error

+  }

+

+  constructor {:verify false} init1()

+  {

+    assert false;

+  }

+

+}