Disallow user-defined attributes that begin with an underscore

1 files changed, 4 insertions, 2 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7a93a140..6081f2c6 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -443,11 +443,13 @@ namespace Microsoft.Dafny {
     }

     public void PrintOneAttribute(Attributes a, string nameSubstitution = null) {

       Contract.Requires(a != null);

-      wr.Write(" {{:{0}", nameSubstitution ?? a.Name);

+      var name = nameSubstitution ?? a.Name;

+      var usAttribute = name.StartsWith("_");

+      wr.Write(" {1}{{:{0}", name, usAttribute ? "/*" : "");

       if (a.Args != null) {

         PrintAttributeArgs(a.Args, false);

       }

-      wr.Write("}");

+      wr.Write("}}{0}", usAttribute ? "*/" : "");

     }

 

     public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {