Dafny: allow attributes on function/method declarations to refer to the (in- and out-)parameters

1 files changed, 6 insertions, 1 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index a3668619..5d806aa9 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -413,8 +413,8 @@ namespace Microsoft.Dafny {
       ResolveAttributes(cl.Attributes, false);

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

-        ResolveAttributes(member.Attributes, false);

         if (member is Field) {

+          ResolveAttributes(member.Attributes, false);

           // nothing more to do

 

         } else if (member is Function) {

@@ -457,6 +457,7 @@ namespace Microsoft.Dafny {
 

         } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

+          ResolveAttributes(member.Attributes, false);

           if (inv.Refined != null) {

             inv.Formals = new List<Formal>();

             scope.PushMarker();

@@ -649,6 +650,7 @@ namespace Microsoft.Dafny {
       foreach (Formal p in f.Formals) {

         scope.Push(p.Name, p);

       }

+      ResolveAttributes(f.Attributes, false);

       foreach (Expression r in f.Req) {

         ResolveExpression(r, false);

         Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression

@@ -779,6 +781,9 @@ namespace Microsoft.Dafny {
         scope.Push(p.Name, p);

       }

 

+      // attributes are allowed to mention both in- and out-parameters

+      ResolveAttributes(m.Attributes, false);

+

       // ... continue resolving specification

       foreach (MaybeFreeExpression e in m.Ens) {

         ResolveExpression(e.E, true);