diff options
author | leino <unknown> | 2014-11-01 13:59:06 -0700 |
---|---|---|
committer | leino <unknown> | 2014-11-01 13:59:06 -0700 |
commit | e200c1f9a8b5e7873b17abc71e4a8c1f953ed31c (patch) | |
tree | 084f3b080f42bf90e3ce15c19a91c72737b65a64 /Source/Dafny/Compiler.cs | |
parent | f21cde811e9194934eb30f196ad19c2cfbeb8ff9 (diff) | |
parent | 02e2b99ab18659ea2626e2be5fa369b7f1795334 (diff) |
Merge
Diffstat (limited to 'Source/Dafny/Compiler.cs')
-rw-r--r-- | Source/Dafny/Compiler.cs | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 9d2cad2f..0c670062 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1120,6 +1120,11 @@ namespace Microsoft.Dafny { if (s.Body == null) {
compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line);
}
+ } else if (stmt is WhileStmt) {
+ var s = (WhileStmt)stmt;
+ if (s.Body == null) {
+ compiler.Error("a while statement without a body cannot be compiled (line {0})", stmt.Tok.line);
+ }
}
}
}
@@ -1388,6 +1393,9 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
+ if (s.Body == null) {
+ return;
+ }
if (s.Guard == null) {
Indent(indent);
wr.WriteLine("while (false) { }");
@@ -2515,7 +2523,7 @@ namespace Microsoft.Dafny { var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);
wr.Write("Dafny.Helpers.Let<");
wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type));
- wr.Write(">(");
+ wr.Write(">(");
TrExpr(e.RHSs[i]);
wr.Write(", " + rhsName + " => ");
neededCloseParens++;
|