Dafny: Added support for attributes on methods and constructors.

2 files changed, 26 insertions, 13 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 6609c43f..cbea8535 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -355,20 +355,20 @@ namespace Microsoft.Boogie {
       }

     }

 

-    void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, 

-                                  List<Implementation/*!*/>/*!*/ loopImpls, 

+    void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,

+                                  List<Implementation/*!*/>/*!*/ loopImpls,

                                   Dictionary<string, Dictionary<string, Block>> fullMap) {

       Contract.Requires(impl != null);

       Contract.Requires(cce.NonNullElements(loopImpls));

-      // Enumerate the headers 

+      // Enumerate the headers

       // for each header h:

-      //   create implementation p_h with 

+      //   create implementation p_h with

       //     inputs = inputs, outputs, and locals of impl

       //     outputs = outputs and locals of impl

       //     locals = empty set

       //   add call o := p_h(i) at the beginning of the header block

       //   break the back edges whose target is h

-      // Enumerate the headers again to create the bodies of p_h 

+      // Enumerate the headers again to create the bodies of p_h

       // for each header h:

       //   compute the loop corresponding to h

       //   make copies of all blocks in the loop for h

@@ -697,7 +697,7 @@ namespace Microsoft.Boogie {
       }

       return g;

     }

-    

+

     public class IrreducibleLoopException : Exception {}

 

     public Graph<Block> ProcessLoops(Implementation impl) {

@@ -2378,6 +2378,19 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

+      : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {

+      Contract.Requires(kv != null);

+      Contract.Requires(structuredStmts != null);

+      Contract.Requires(localVariables != null);

+      Contract.Requires(outParams != null);

+      Contract.Requires(inParams != null);

+      Contract.Requires(typeParams != null);

+      Contract.Requires(name != null);

+      Contract.Requires(tok != null);

+      //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());

+    }

+

     public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) {

       Contract.Requires(structuredStmts != null);

@@ -3232,11 +3245,11 @@ namespace Microsoft.Boogie {
       Contract.Requires(varSeq != null);

     }

     /*  PR: the following two constructors cause Spec# crashes

-        public TypeVariableSeq(TypeVariable! var) 

+        public TypeVariableSeq(TypeVariable! var)

           : base(new TypeVariable! [] { var })

         {

         }

-        public TypeVariableSeq() 

+        public TypeVariableSeq()

           : base(new TypeVariable![0])

         {

         } */

@@ -3723,4 +3736,4 @@ namespace Microsoft.Boogie {
       }

     }

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0c5be389..a1058786 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -89,7 +89,7 @@ namespace Microsoft.Dafny {
 

         return new Bpl.TypeSynonymAnnotation(Token.NoToken, multiSetTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

@@ -1071,7 +1071,7 @@ namespace Microsoft.Dafny {
 

       Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,

         typeParams, inParams, outParams,

-        localVariables, stmts);

+        localVariables, stmts, etran.TrAttributes(m.Attributes));

       sink.TopLevelDeclarations.Add(impl);

 

       currentMethod = null;

@@ -4973,7 +4973,7 @@ namespace Microsoft.Dafny {
               return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);

             case BinaryExpr.ResolvedOpcode.SetDifference:

               return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);

- 

+

             case BinaryExpr.ResolvedOpcode.MultiSetEq:

               return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1);

             case BinaryExpr.ResolvedOpcode.MultiSetNeq:

@@ -5359,7 +5359,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType)), Bpl.Expr.Literal(0));

       }

 

-      Bpl.QKeyValue TrAttributes(Attributes attrs) {

+      public Bpl.QKeyValue TrAttributes(Attributes attrs) {

         Bpl.QKeyValue kv = null;

         while (attrs != null) {

           List<object> parms = new List<object>();