diff options
| author |  qunyanm <unknown> | 2016-03-31 14:43:46 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2016-03-31 14:43:46 -0700 |
| commit | 31b0c4345b02b2314ca92a032ce90fbfdf66d1e8 (patch) | |
| tree | a7b46d9a6db9f6cdf8d9197fc44354bc0462c27e | |
| parent | 8b9126340fb1b5c5c4abe67b940911b675d22c63 (diff) | |
Allow modifies clauses for a "Main" method annotated with {:main} attribute.
| -rw-r--r-- | Source/Dafny/Compiler.cs | 4 |
1 files 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 {
|