diff options
| author |  Rustan Leino <unknown> | 2013-11-14 17:17:14 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-11-14 17:17:14 -0800 |
| commit | efb6efa4fa204c46b4d8ca5e989eb2a088b5a710 (patch) | |
| tree | 7b0bf8a27693060d7766639b503fac64432973c3 /Source/Dafny/Compiler.cs | |
| parent | 0975663860053e1ed568b971abb1e0d25cc48f3a (diff) | |
Let compiler complain about body-less functions and methods, even if these are ghost
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 5fd70652..f91f53d1 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -686,10 +686,10 @@ namespace Microsoft.Dafny { } else if (member is Function) {
Function f = (Function)member;
- if (f.IsGhost) {
- // nothing to compile
- } else if (f.Body == null) {
+ if (f.Body == null) {
Error("Function {0} has no body", f.FullName);
+ } else if (f.IsGhost) {
+ // nothing to compile
} else {
Indent(indent);
wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
@@ -700,12 +700,14 @@ namespace Microsoft.Dafny { WriteFormals("", f.Formals);
wr.WriteLine(") {");
CompileReturnBody(f.Body, indent + IndentAmount);
- Indent(indent); wr.WriteLine("}");
+ Indent(indent); wr.WriteLine("}");
}
} else if (member is Method) {
Method m = (Method)member;
- if (!m.IsGhost) {
+ if (m.IsGhost && m.Body == null) {
+ Error("Method {0} has no body", m.FullName);
+ } else if (!m.IsGhost) {
Indent(indent);
wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);
if (m.TypeArgs.Count != 0) {
|