From 62eb04905d6dcb3ab0b6d7cbf1051c97fec01474 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 28 Mar 2016 14:51:00 -0700
Subject: Allow users to annontate a method as main with {:main} attribute.
 It’s an error if more than one method is so annotated. For that method, the
 usual restrictions for "main" apply, but 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, modeled, for example,
 via ghost parameters.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Source/Dafny/Compiler.cs | 73 +++++++++++++++++++++++++++++++++++-------------
 1 file changed, 53 insertions(+), 20 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d6b2d9ba..8af2cb24 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -757,34 +757,63 @@ namespace Microsoft.Dafny {
     }
 
     public bool HasMain(Program program) {
+      Method mainMethod = null;
+      bool hasMain = false;
       foreach (var module in program.Modules) {
+        if (module.IsAbstract) {
+          // the purpose of an abstract module is to skip compilation
+          continue;
+        }
         foreach (var decl in module.TopLevelDecls) {
           var c = decl as ClassDecl;
           if (c != null) {
             foreach (var member in c.Members) {
               var m = member as Method;
               if (m != null && IsMain(m)) {
-                  return true;
+                if (mainMethod == null) {
+                  mainMethod = m;
+                  hasMain = true;
+                } else {
+                  // more than one main in the program
+                  ErrorWriter.WriteLine("More than one method is declared as \"main\"");
+                  ErrorCount++;
+                  hasMain = false;
+                }
               }
             }
           }
         }
       }
-      return false;
+      return hasMain;
     }
 
     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 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 
+      // 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, 
+      //    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 {
+      } 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)) {
+        if (m.Ins.Count == 0) {
+          return true;
+        } else {
+          bool isGhost = true;
+          foreach (var arg in m.Ins) {
+            if (!arg.IsGhost) {
+              isGhost = false;
+            }
+          }
+          return isGhost;
+        }
+      } else {
         return false;
       }
     }
@@ -951,24 +980,28 @@ namespace Microsoft.Dafny {
       Indent(indent, wr); wr.WriteLine("}");
 
       // allow the Main method to be an instance method
-      if (!m.IsStatic && IsMain(m)) {
+      if (IsMain(m) && (!m.IsStatic || m.CompileName != "Main")) {
         Indent(indent, wr);
         wr.WriteLine("public static void Main(string[] args) {");
-        Contract.Assert(m.EnclosingClass == c);
-        Indent(indent + IndentAmount, wr);
-        wr.Write("@{0} b = new @{0}", c.CompileName);
-        if (c.TypeArgs.Count != 0) {
-          // instantiate every parameter, it doesn't particularly matter how
-          wr.Write("<");
-          string sep = "";
-          for (int i = 0; i < c.TypeArgs.Count; i++) {
-            wr.Write("{0}int", sep);
-            sep = ", ";
+        if (!m.IsStatic) {
+          Contract.Assert(m.EnclosingClass == c);
+          Indent(indent + IndentAmount, wr);
+          wr.Write("@{0} b = new @{0}", c.CompileName);
+          if (c.TypeArgs.Count != 0) {
+            // instantiate every parameter, it doesn't particularly matter how
+            wr.Write("<");
+            string sep = "";
+            for (int i = 0; i < c.TypeArgs.Count; i++) {
+              wr.Write("{0}int", sep);
+              sep = ", ";
+            }
+            wr.Write(">");
           }
-          wr.Write(">");
+          wr.WriteLine("();");
+          Indent(indent + IndentAmount, wr); wr.WriteLine("b.@{0}();", m.CompileName);
+        } else {
+          Indent(indent + IndentAmount, wr); wr.WriteLine("@{0}();", m.CompileName);
         }
-        wr.WriteLine("();");
-        Indent(indent + IndentAmount, wr); wr.WriteLine("b.@Main();");
         Indent(indent, wr); wr.WriteLine("}");
       }
     }
-- 
cgit v1.2.3