summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-03-28 14:51:00 -0700
committerGravatar qunyanm <unknown>2016-03-28 14:51:00 -0700
commit62eb04905d6dcb3ab0b6d7cbf1051c97fec01474 (patch)
tree002242ed44f718fc916ac83643ffdc5682260b3d
parent91cee1c2028f9ad995df863f2a4568d95f4ea1a8 (diff)
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.
-rw-r--r--Source/Dafny/Compiler.cs73
1 files changed, 53 insertions, 20 deletions
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("}");
}
}