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

4 files changed, 43 insertions, 33 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 67347e2a..34dde196 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -698,7 +698,7 @@ UpdateStmt<out Statement/*!*/ s>
   .)

   Lhs<out e>                       (. x = e.tok; .)

   ( { IF(IsAttribute()) Attribute<ref attrs> }

-    ";"                            (. rhss.Add(new ExprRhs(e)); .)

+    ";"                            (. rhss.Add(new ExprRhs(e, attrs)); .)

   |                                (. lhss.Add(e);  lhs0 = e; .)

     { "," Lhs<out e>               (. lhss.Add(e); .)

     }

@@ -706,11 +706,10 @@ UpdateStmt<out Statement/*!*/ s>
     Rhs<out r, lhs0>               (. rhss.Add(r); .)

     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

-    { IF(IsAttribute()) Attribute<ref attrs> }

     ";"

   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)

   )

-  (. s = new UpdateStmt(x, lhss, rhss, attrs); .)

+  (. s = new UpdateStmt(x, lhss, rhss); .)

   .

 Rhs<out AssignmentRhs r, Expression receiverForInitCall>

 = (. IToken/*!*/ x, newToken;  Expression/*!*/ e;

@@ -719,6 +718,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
      CallStmt initCall = null;

      List<Expression> args;

      r = null;  // to please compiler

+     Attributes attrs = null;

   .)

   ( "new"                              (. newToken = t; .)

     TypeAndToken<out x, out ty>

@@ -745,6 +745,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
   | "*"                                (. r = new HavocRhs(t); .)

   | Expression<out e>                  (. r = new ExprRhs(e); .)

   )

+  { IF(IsAttribute()) Attribute<ref attrs> }     (. r.Attributes = attrs; .)

   .

 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

@@ -752,7 +753,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
      AssignmentRhs r;  IdentifierExpr lhs0;

      List<VarDecl> lhss = new List<VarDecl>();

      List<AssignmentRhs> rhss = new List<AssignmentRhs>();

-     Attributes attrs = null;

   .)

   [ "ghost"                                 (. isGhost = true;  x = t; .)

   ]

@@ -768,7 +768,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
     Rhs<out r, lhs0>               (. rhss.Add(r); .)

     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

-    { IF(IsAttribute()) Attribute<ref attrs> }

   ]

   ";"

   (. UpdateStmt update;

@@ -779,7 +778,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
        foreach (var lhs in lhss) {

          ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

        }

-       update = new UpdateStmt(assignTok, ies, rhss, attrs);

+       update = new UpdateStmt(assignTok, ies, rhss);

      }

      s = new VarDeclStmt(x, lhss, update);

   .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1470c0b3..be062fba 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1412,8 +1412,28 @@ namespace Microsoft.Dafny {
 

   public abstract class AssignmentRhs {

     public readonly IToken Tok;

-    internal AssignmentRhs(IToken tok) {

+

+    private Attributes attributes;

+    public Attributes Attributes

+    {

+      get

+      {

+        return attributes;

+      }

+      set

+      {

+        attributes = value;

+      }

+    }

+

+    public bool HasAttributes()

+    {

+      return Attributes != null;

+    }

+

+    internal AssignmentRhs(IToken tok, Attributes attrs = null) {

       Tok = tok;

+      Attributes = attrs;

     }

     public abstract bool CanAffectPreviouslyKnownExpressions { get; }

   }

@@ -1426,8 +1446,8 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Expr != null);

     }

 

-    public ExprRhs(Expression expr)

-      : base(expr.tok)

+    public ExprRhs(Expression expr, Attributes attrs = null)

+      : base(expr.tok, attrs)

     {

       Contract.Requires(expr != null);

       Expr = expr;

@@ -1567,7 +1587,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(Lhss));

       Contract.Invariant(cce.NonNullElements(Rhss));

     }

-    public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, Attributes attrs = null)

+    public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss)

       : base(tok)

     {

       Contract.Requires(tok != null);

@@ -1577,9 +1597,8 @@ namespace Microsoft.Dafny {
       Lhss = lhss;

       Rhss = rhss;

       CanMutateKnownState = false;

-      Attributes = attrs;

     }

-    public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate, Attributes attrs = null)

+    public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)

       : base(tok)

     {

       Contract.Requires(tok != null);

@@ -1589,7 +1608,6 @@ namespace Microsoft.Dafny {
       Lhss = lhss;

       Rhss = rhss;

       CanMutateKnownState = mutate;

-      Attributes = attrs;

     }

   }

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 371bb2c8..52f86e5f 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1135,7 +1135,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Attribute(ref attrs);

 			}

 			Expect(18);

-			rhss.Add(new ExprRhs(e)); 

+			rhss.Add(new ExprRhs(e, attrs)); 

 		} else if (la.kind == 20 || la.kind == 50) {

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 20) {

@@ -1152,15 +1152,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Rhs(out r, lhs0);

 				rhss.Add(r); 

 			}

-			while (IsAttribute()) {

-				Attribute(ref attrs);

-			}

 			Expect(18);

 		} else if (la.kind == 5) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

 		} else SynErr(136);

-		s = new UpdateStmt(x, lhss, rhss, attrs); 

+		s = new UpdateStmt(x, lhss, rhss); 

 	}

 

 	void VarDeclStatement(out Statement/*!*/ s) {

@@ -1169,7 +1166,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		AssignmentRhs r;  IdentifierExpr lhs0;

 		List<VarDecl> lhss = new List<VarDecl>();

 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();

-		Attributes attrs = null;

 		

 		if (la.kind == 12) {

 			Get();

@@ -1197,9 +1193,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Rhs(out r, lhs0);

 				rhss.Add(r); 

 			}

-			while (IsAttribute()) {

-				Attribute(ref attrs);

-			}

 		}

 		Expect(18);

 		UpdateStmt update;

@@ -1210,7 +1203,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 foreach (var lhs in lhss) {

 		   ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

 		 }

-		 update = new UpdateStmt(assignTok, ies, rhss, attrs);

+		 update = new UpdateStmt(assignTok, ies, rhss);

 		}

 		s = new VarDeclStmt(x, lhss, update);

 		

@@ -1352,6 +1345,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		CallStmt initCall = null;

 		List<Expression> args;

 		r = null;  // to please compiler

+		Attributes attrs = null;

 		

 		if (la.kind == 51) {

 			Get();

@@ -1396,6 +1390,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

 			r = new ExprRhs(e); 

 		} else SynErr(140);

+		while (IsAttribute()) {

+			Attribute(ref attrs);

+		}

+		r.Attributes = attrs; 

 	}

 

 	void Lhs(out Expression e) {

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7649fa11..cf8be27e 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -641,11 +641,6 @@ namespace Microsoft.Dafny {
           sep = ", ";

         }

 

-        if (stmt.HasAttributes())

-        {

-          PrintAttributes(stmt.Attributes);

-        }

-

         wr.Write(";");

 

       } else if (stmt is VarDeclStmt) {

@@ -668,11 +663,6 @@ namespace Microsoft.Dafny {
             PrintRhs(rhs);

             sep = ", ";

           }

-

-          if (s.Update.HasAttributes())

-          {

-            PrintAttributes(s.Update.Attributes);

-          }

         }

         wr.Write(";");

 

@@ -723,6 +713,11 @@ namespace Microsoft.Dafny {
       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

       }

+

+      if (rhs.HasAttributes())

+      {

+        PrintAttributes(rhs.Attributes);

+      }

     }

 

     void PrintGuard(Expression guard) {