From 31b0c4345b02b2314ca92a032ce90fbfdf66d1e8 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 31 Mar 2016 14:43:46 -0700
Subject: Allow modifies clauses for a "Main" method annotated with {:main}
 attribute.

---
 Source/Dafny/Compiler.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 8af2cb24..66765b34 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -795,13 +795,13 @@ namespace Microsoft.Dafny {
       //    The method has no modifies clause 
       //    If the method is an instance (that is, non-static) method in a class, then the enclosing class must not declare any constructor
       // Or if a method is annotated with {:main} and the above restrictions apply, except it is allowed to take ghost arguments, 
-      //    and it is allowed to have preconditions.  This lets the programmer add some explicit assumptions about the outside world, 
+      //    and it is allowed to have preconditions and modifies.  This lets the programmer add some explicit assumptions about the outside world, 
       //    modeled, for example, via ghost parameters.
       if (!m.IsGhost && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0
             && m.Mod.Expressions.Count == 0 && (m.IsStatic || (((ClassDecl)m.EnclosingClass) == null) || !((ClassDecl)m.EnclosingClass).HasConstructor)) {
         return true;
       } else if (Attributes.Contains(m.Attributes, "main") && !m.IsGhost && m.TypeArgs.Count == 0 && m.Outs.Count == 0
-            && m.Mod.Expressions.Count == 0 && (m.IsStatic || (((ClassDecl)m.EnclosingClass) == null) || !((ClassDecl)m.EnclosingClass).HasConstructor)) {
+            && (m.IsStatic || (((ClassDecl)m.EnclosingClass) == null) || !((ClassDecl)m.EnclosingClass).HasConstructor)) {
         if (m.Ins.Count == 0) {
           return true;
         } else {
-- 
cgit v1.2.3