Fix issue #62. Check for modifies clause and constructors in the enclosing

class when determining whether a method named Main() is the program entry.

2 files changed, 32 insertions, 5 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 08375fae..e557e509 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -731,10 +731,8 @@ namespace Microsoft.Dafny {
           if (c != null) {

             foreach (var member in c.Members) {

               var m = member as Method;

-              if (m != null) {

-                if (!m.IsGhost && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0) {

+              if (m != null && IsMain(m)) {

                   return true;

-                }

               }

             }

           }

@@ -743,6 +741,23 @@ namespace Microsoft.Dafny {
       return false;

     }

 

+    public static bool IsMain(Method m) {

+      // In order to be a legal Main() method, the following must be true:

+      //    The method takes no parameters 

+      //    The method is not a ghost method 

+      //    The method has no requires clause 

+      //    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

+      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 {

+        return false;

+      }

+    }

+

+

     void CompileClassMembers(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

@@ -904,9 +919,9 @@ namespace Microsoft.Dafny {
                   }

                   Indent(indent); wr.WriteLine("}");

 

+                

                   // allow the Main method to be an instance method

-                  if (!m.IsStatic && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0)

-                  {

+                 if (!m.IsStatic && IsMain(m)) {               

                       Indent(indent);

                       wr.WriteLine("public static void Main(string[] args) {");

                       Contract.Assert(m.EnclosingClass == c);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 14c1b35e..ed089f10 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3136,6 +3136,18 @@ namespace Microsoft.Dafny {
         return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr);

       }

     }

+

+    public override string CompileName {

+      get {

+        var nm = base.CompileName;

+        if (IsStatic && nm == "Main" && !Dafny.Compiler.IsMain(this)) {

+          // for a static method that is named "Main" but is not a legal "Main" method,

+          // change its name.

+          nm = EnclosingClass.Name + "_" + nm;

+        }

+        return nm;

+      }

+    } 

   }

 

   public class Lemma : Method