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 | |
parent | 0975663860053e1ed568b971abb1e0d25cc48f3a (diff) |
Let compiler complain about body-less functions and methods, even if these are ghost
Diffstat (limited to 'Source/Dafny')
-rw-r--r-- | Source/Dafny/Compiler.cs | 12 | ||||
-rw-r--r-- | Source/Dafny/Printer.cs | 2 |
2 files changed, 9 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) {
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index b82a7169..767d24b8 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1454,6 +1454,8 @@ namespace Microsoft.Dafny { // this is not expected for a parsed program, but we may be called for /trace purposes in the translator
var e = (BoxingCastExpr)expr;
PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);
+ } else if (expr is Translator.BoogieWrapper) {
+ wr.Write("[BoogieWrapper]"); // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
|