From e7bf7ffb17f0c4022c3df81b4fe33df440723c37 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 26 Oct 2011 21:49:27 -0700
Subject: Dafny: allow attributes on function/method declarations to refer to
 the (in- and out-)parameters

---
 Dafny/Resolver.cs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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);
-- 
cgit v1.2.3