Dafny:

* fixed ghost/non-ghost story for breaks and returns
* changed compilation/translation to always use goto's to implement Dafny's breaks
* introduced "break break" statements

11 files changed, 638 insertions, 159 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index fdab9ab9..82604794 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -609,14 +609,9 @@ namespace Microsoft.Dafny {
           wr.WriteLine(");");

         }

       } else if (stmt is BreakStmt) {

-        BreakStmt s = (BreakStmt)stmt;

+        var s = (BreakStmt)stmt;

         Indent(indent);

-        if (s.TargetLabel == null) {

-          // use the scoping rules of C#

-          wr.WriteLine("break;");

-        } else {

-          wr.WriteLine("goto after_{0};", s.TargetLabel);

-        }

+        wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);

       } else if (stmt is ReturnStmt) {

         Indent(indent);

         wr.WriteLine("return;");

@@ -927,29 +922,11 @@ namespace Microsoft.Dafny {
     }

     

     void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));

-      List<string/*!*/> currentLabels = null;

       foreach (Statement ss in stmts) {

-        if (ss is LabelStmt) {

-          LabelStmt s = (LabelStmt)ss;

-          if (currentLabels == null) {

-            currentLabels = new List<string>();

-          }

-          currentLabels.Add(s.Label);

-        } else {

-          TrStmt(ss, indent + IndentAmount);

-          SpillLabels(currentLabels, indent);

-          currentLabels = null;

-        }

-      }

-      SpillLabels(currentLabels, indent);

-    }

-

-    void SpillLabels(List<string> labels, int indent) {

-      Contract.Requires(cce.NonNullElements(labels));

-      if (labels != null) {

-        foreach (string label in labels) {

-          Indent(indent);

-          wr.WriteLine("after_{0}: ;", label);

+        TrStmt(ss, indent + IndentAmount);

+        if (ss.Labels != null) {

+          Indent(indent);  // labels are not indented as much as the statements

+          wr.WriteLine("after_{0}: ;", ss.Labels.UniqueId);

         }

       }

     }

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index b7b81d44..e3761d57 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -434,7 +434,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
   { Attribute<ref attrs> }

   Ident<out id>

   [ GenericParameters<typeArgs> ]

-  Formals<true, true, ins>

+  Formals<true, !mmod.IsGhost, ins>

   [ "returns"

     Formals<false, true, outs>

   ]

@@ -579,7 +579,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   { Attribute<ref attrs> }

   Ident<out id> 

   [ GenericParameters<typeArgs> ]

-  Formals<true, false, formals>

+  Formals<true, isFunctionMethod, formals>

   ":"

   Type<out returnType>

   ( ";"

@@ -710,6 +710,7 @@ OneStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  IToken/*!*/ id;  string label = null;

      s = dummyStmt;  /* to please the compiler */

      IToken bodyStart, bodyEnd;

+     int breakCount;

   .)

   /* This list does not contain BlockStmt, see comment above in Stmt production. */

   ( BlockStmt<out s, out bodyStart, out bodyEnd>

@@ -725,10 +726,14 @@ OneStmt<out Statement/*!*/ s>
   | MatchStmt<out s>

   | ForeachStmt<out s>

   | "label"                            (. x = t; .)

-    Ident<out id> ":"                  (. s = new LabelStmt(x, id.val); .)

-  | "break"                            (. x = t; .)

-    [ Ident<out id>                    (. label = id.val; .)

-    ] ";"                              (. s = new BreakStmt(x, label); .)

+    Ident<out id> ":"

+    OneStmt<out s>                     (. s.Labels = new LabelNode(x, id.val, s.Labels); .)

+  | "break"                            (. x = t; breakCount = 1; label = null; .)

+    ( Ident<out id>                    (. label = id.val; .)

+    | { "break"                        (. breakCount++; .)

+      }

+    )

+    ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)

   | "return"                           (. x = t; .)

     ";"                                (. s = new ReturnStmt(x); .)

   )

@@ -751,6 +756,7 @@ UpdateStmt<out Statement/*!*/ s>
     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)

     }

     ";"

+  | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)

   )

   (. s = new UpdateStmt(x, lhss, rhss); .)

   .

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 8d1143af..bb5f4f67 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1141,6 +1141,8 @@ namespace Microsoft.Dafny {
 

   public abstract class Statement {

     public readonly IToken Tok;

+    public LabelNode Labels;  // mutable during resolution

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Tok != null);

@@ -1153,7 +1155,25 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public abstract class PredicateStmt : Statement {

+  public class LabelNode

+  {

+    public readonly IToken Tok;

+    public readonly string Label;

+    public readonly int UniqueId;

+    public readonly LabelNode Next;

+    static int nodes = 0;

+

+    public LabelNode(IToken tok, string label, LabelNode next) {

+      Contract.Requires(tok != null);

+      Tok = tok;

+      Label = label;

+      Next = next;

+      UniqueId = nodes++;

+    }

+  }

+

+  public abstract class PredicateStmt : Statement

+  {

     [Peer]

     public readonly Expression Expr;

     [ContractInvariantMethod]

@@ -1255,31 +1275,25 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class LabelStmt : Statement {

-    public readonly string Label;

+  public class BreakStmt : Statement {

+    public readonly string TargetLabel;

+    public readonly int BreakCount;

+    public Statement TargetStmt;  // filled in during resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Label != null);

+      Contract.Invariant(TargetLabel == null || 1 <= BreakCount);

     }

 

-    public LabelStmt(IToken/*!*/ tok, string/*!*/ label)

+    public BreakStmt(IToken tok, string targetLabel)

       : base(tok) {

       Contract.Requires(tok != null);

-      Contract.Requires(label != null);

-      this.Label = label;

-

+      this.TargetLabel = targetLabel;

     }

-  }

-

-  public class BreakStmt : Statement {

-    public readonly string TargetLabel;

-    public Statement TargetStmt;  // filled in during resolution

-

-    public BreakStmt(IToken tok, string targetLabel)

+    public BreakStmt(IToken tok, int breakCount)

       : base(tok) {

       Contract.Requires(tok != null);

-      this.TargetLabel = targetLabel;

-

+      Contract.Requires(1 <= breakCount);

+      this.BreakCount = breakCount;

     }

   }

 

@@ -1287,7 +1301,6 @@ namespace Microsoft.Dafny {
     public ReturnStmt(IToken tok)

       : base(tok) {

       Contract.Requires(tok != null);

-

     }

   }

 

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 2fa88a69..1d7eb3e6 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -466,7 +466,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (la.kind == 23) {

 			GenericParameters(typeArgs);

 		}

-		Formals(true, false, formals);

+		Formals(true, isFunctionMethod, formals);

 		Expect(22);

 		Type(out returnType);

 		if (la.kind == 15) {

@@ -518,7 +518,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (la.kind == 23) {

 			GenericParameters(typeArgs);

 		}

-		Formals(true, true, ins);

+		Formals(true, !mmod.IsGhost, ins);

 		if (la.kind == 26) {

 			Get();

 			Formals(false, true, outs);

@@ -996,6 +996,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  IToken/*!*/ id;  string label = null;

 		s = dummyStmt;  /* to please the compiler */

 		IToken bodyStart, bodyEnd;

+		int breakCount;

 		

 		if (la.kind == 7) {

 			BlockStmt(out s, out bodyStart, out bodyEnd);

@@ -1026,22 +1027,28 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t; 

 			Ident(out id);

 			Expect(22);

-			s = new LabelStmt(x, id.val); 

+			OneStmt(out s);

+			s.Labels = new LabelNode(x, id.val, s.Labels); 

 		} else if (la.kind == 48) {

 			Get();

-			x = t; 

+			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

-			}

+			} else if (la.kind == 15 || la.kind == 48) {

+				while (la.kind == 48) {

+					Get();

+					breakCount++; 

+				}

+			} else SynErr(120);

 			Expect(15);

-			s = new BreakStmt(x, label); 

+			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 		} else if (la.kind == 49) {

 			Get();

 			x = t; 

 			Expect(15);

 			s = new ReturnStmt(x); 

-		} else SynErr(120);

+		} else SynErr(121);

 	}

 

 	void AssertStmt(out Statement/*!*/ s) {

@@ -1117,7 +1124,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 				rhss.Add(r); 

 			}

 			Expect(15);

-		} else SynErr(121);

+		} else if (la.kind == 22) {

+			Get();

+			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

+		} else SynErr(122);

 		s = new UpdateStmt(x, lhss, rhss); 

 	}

 

@@ -1199,13 +1209,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 				} else if (la.kind == 7) {

 					BlockStmt(out s, out bodyStart, out bodyEnd);

 					els = s; 

-				} else SynErr(122);

+				} else SynErr(123);

 			}

 			ifStmt = new IfStmt(x, guard, thn, els); 

 		} else if (la.kind == 7) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(123);

+		} else SynErr(124);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1230,7 +1240,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); 

-		} else SynErr(124);

+		} else SynErr(125);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

@@ -1295,7 +1305,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 56) {

 			HavocStmt(out s);

 			bodyAssign = s; 

-		} else SynErr(125);

+		} else SynErr(126);

 		Expect(8);

 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

@@ -1319,7 +1329,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(126);

+		} else SynErr(127);

 	}

 

 	void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {

@@ -1369,7 +1379,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(127);

+		} else SynErr(128);

 	}

 

 	void Guard(out Expression e) {

@@ -1381,7 +1391,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(128);

+		} else SynErr(129);

 		Expect(33);

 	}

 

@@ -1471,7 +1481,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else SynErr(129);

+		} else SynErr(130);

 	}

 

 	void EquivExpression(out Expression/*!*/ e0) {

@@ -1501,7 +1511,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 68) {

 			Get();

-		} else SynErr(130);

+		} else SynErr(131);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

@@ -1539,7 +1549,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 70) {

 			Get();

-		} else SynErr(131);

+		} else SynErr(132);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e0) {

@@ -1557,7 +1567,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 72) {

 			Get();

-		} else SynErr(132);

+		} else SynErr(133);

 	}

 

 	void OrOp() {

@@ -1565,7 +1575,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 74) {

 			Get();

-		} else SynErr(133);

+		} else SynErr(134);

 	}

 

 	void Term(out Expression/*!*/ e0) {

@@ -1641,7 +1651,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(134); break;

+		default: SynErr(135); break;

 		}

 	}

 

@@ -1663,7 +1673,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 85) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(135);

+		} else SynErr(136);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

@@ -1690,7 +1700,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 52 || la.kind == 54) {

 				Suffix(ref e);

 			}

-		} else SynErr(136);

+		} else SynErr(137);

 	}

 

 	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

@@ -1704,7 +1714,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 87) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(137);

+		} else SynErr(138);

 	}

 

 	void NegOp() {

@@ -1712,7 +1722,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 89) {

 			Get();

-		} else SynErr(138);

+		} else SynErr(139);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1733,7 +1743,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			QuantifierGuts(out e);

 		} else if (la.kind == 37) {

 			ComprehensionExpr(out e);

-		} else SynErr(139);

+		} else SynErr(140);

 	}

 

 	void DottedIdentifiersAndFunction(out Expression e) {

@@ -1806,12 +1816,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(140);

+				} else SynErr(141);

 			} else if (la.kind == 98) {

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else SynErr(141);

+			} else SynErr(142);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -1835,7 +1845,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}

 			

 			Expect(53);

-		} else SynErr(142);

+		} else SynErr(143);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -1932,7 +1942,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(33);

 			break;

 		}

-		default: SynErr(143); break;

+		default: SynErr(144); break;

 		}

 	}

 

@@ -1963,7 +1973,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 101 || la.kind == 102) {

 			Exists();

 			x = t; 

-		} else SynErr(144);

+		} else SynErr(145);

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

 		while (la.kind == 19) {

@@ -2021,7 +2031,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 100) {

 			Get();

-		} else SynErr(145);

+		} else SynErr(146);

 	}

 

 	void Exists() {

@@ -2029,7 +2039,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 102) {

 			Get();

-		} else SynErr(146);

+		} else SynErr(147);

 	}

 

 	void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

@@ -2042,7 +2052,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			es = new List<Expression/*!*/>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else SynErr(147);

+		} else SynErr(148);

 		Expect(8);

 	}

 

@@ -2051,7 +2061,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 104) {

 			Get();

-		} else SynErr(148);

+		} else SynErr(149);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2250,34 +2260,35 @@ public class Errors {
 			case 118: s = "invalid PossiblyWildExpression"; break;

 			case 119: s = "invalid MatchOrExpr"; break;

 			case 120: s = "invalid OneStmt"; break;

-			case 121: s = "invalid UpdateStmt"; break;

-			case 122: s = "invalid IfStmt"; break;

+			case 121: s = "invalid OneStmt"; break;

+			case 122: s = "invalid UpdateStmt"; break;

 			case 123: s = "invalid IfStmt"; break;

-			case 124: s = "invalid WhileStmt"; break;

-			case 125: s = "invalid ForeachStmt"; break;

-			case 126: s = "invalid Lhs"; break;

-			case 127: s = "invalid Rhs"; break;

-			case 128: s = "invalid Guard"; break;

-			case 129: s = "invalid AttributeArg"; break;

-			case 130: s = "invalid EquivOp"; break;

-			case 131: s = "invalid ImpliesOp"; break;

-			case 132: s = "invalid AndOp"; break;

-			case 133: s = "invalid OrOp"; break;

-			case 134: s = "invalid RelOp"; break;

-			case 135: s = "invalid AddOp"; break;

-			case 136: s = "invalid UnaryExpression"; break;

-			case 137: s = "invalid MulOp"; break;

-			case 138: s = "invalid NegOp"; break;

-			case 139: s = "invalid EndlessExpression"; break;

-			case 140: s = "invalid Suffix"; break;

+			case 124: s = "invalid IfStmt"; break;

+			case 125: s = "invalid WhileStmt"; break;

+			case 126: s = "invalid ForeachStmt"; break;

+			case 127: s = "invalid Lhs"; break;

+			case 128: s = "invalid Rhs"; break;

+			case 129: s = "invalid Guard"; break;

+			case 130: s = "invalid AttributeArg"; break;

+			case 131: s = "invalid EquivOp"; break;

+			case 132: s = "invalid ImpliesOp"; break;

+			case 133: s = "invalid AndOp"; break;

+			case 134: s = "invalid OrOp"; break;

+			case 135: s = "invalid RelOp"; break;

+			case 136: s = "invalid AddOp"; break;

+			case 137: s = "invalid UnaryExpression"; break;

+			case 138: s = "invalid MulOp"; break;

+			case 139: s = "invalid NegOp"; break;

+			case 140: s = "invalid EndlessExpression"; break;

 			case 141: s = "invalid Suffix"; break;

 			case 142: s = "invalid Suffix"; break;

-			case 143: s = "invalid ConstAtomExpression"; break;

-			case 144: s = "invalid QuantifierGuts"; break;

-			case 145: s = "invalid Forall"; break;

-			case 146: s = "invalid Exists"; break;

-			case 147: s = "invalid AttributeOrTrigger"; break;

-			case 148: s = "invalid QSep"; break;

+			case 143: s = "invalid Suffix"; break;

+			case 144: s = "invalid ConstAtomExpression"; break;

+			case 145: s = "invalid QuantifierGuts"; break;

+			case 146: s = "invalid Forall"; break;

+			case 147: s = "invalid Exists"; break;

+			case 148: s = "invalid AttributeOrTrigger"; break;

+			case 149: s = "invalid QSep"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index f5fba723..c92b477a 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -396,6 +396,13 @@ namespace Microsoft.Dafny {
     /// </summary>

     public void PrintStatement(Statement stmt, int indent) {

       Contract.Requires(stmt != null);

+      for (LabelNode label = stmt.Labels; label != null; label = label.Next) {

+        if (label.Label != null) {

+          wr.WriteLine("label {0}:", label.Label);

+          Indent(indent);

+        }

+      }

+        

       if (stmt is AssertStmt) {

         wr.Write("assert ");

         PrintExpression(((AssertStmt)stmt).Expr);

@@ -417,15 +424,17 @@ namespace Microsoft.Dafny {
         PrintAttributeArgs(s.Args);

         wr.Write(";");

         

-      } else if (stmt is LabelStmt) {

-        wr.Write("label {0}:", ((LabelStmt)stmt).Label);

-        

       } else if (stmt is BreakStmt) {

         BreakStmt s = (BreakStmt)stmt;

-        if (s.TargetLabel == null) {

-          wr.Write("break;");

-        } else {

+        if (s.TargetLabel != null) {

           wr.Write("break {0};", s.TargetLabel);

+        } else {

+          string sep = "";

+          for (int i = 0; i < s.BreakCount; i++) {

+            wr.Write("{0}break", sep);

+            sep = " ";

+          }

+          wr.Write(";");

         }

         

       } else if (stmt is ReturnStmt) {

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index a7fe06ec..3eb3bd34 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -277,6 +277,8 @@ namespace Microsoft.Dafny {
     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();

     readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();

     readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();

+    readonly List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)

+    readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"

     

     /// <summary>

     /// Assumes type parameters have already been pushed

@@ -1118,11 +1120,14 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected restricted-proxy type

       }

     }

-    

+

+    /// <summary>

+    /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it

+    /// at run time.  That means it must not have any side effects on non-ghost variables, for example.

+    /// </summary>

     public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {

       Contract.Requires(stmt != null);

       Contract.Requires(method != null);

-      Contract.Requires(!(stmt is LabelStmt));  // these should be handled inside lists of statements

       if (stmt is UseStmt) {

         UseStmt s = (UseStmt)stmt;

         s.IsGhost = true;

@@ -1153,21 +1158,36 @@ namespace Microsoft.Dafny {
         }

           

       } else if (stmt is BreakStmt) {

-        BreakStmt s = (BreakStmt)stmt;

+        var s = (BreakStmt)stmt;

         if (s.TargetLabel != null) {

           Statement target = labeledStatements.Find(s.TargetLabel);

           if (target == null) {

             Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel);

           } else {

             s.TargetStmt = target;

+            bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;

+            if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {

+              Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));

+            }

+          }

+        } else {

+          if (loopStack.Count < s.BreakCount) {

+            Error(s, "trying to break out of more loop levels than there are enclosing loops");

+          } else {

+            Statement target = loopStack[loopStack.Count - s.BreakCount];

+            if (target.Labels == null) {

+              // make sure there is a label, because the compiler and translator will want to see a unique ID

+              target.Labels = new LabelNode(target.Tok, null, null);

+            }

+            s.TargetStmt = target;

+            if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {

+              Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost loop");

+            }

           }

-        }

-        if (specContextOnly) {

-          Error(stmt, "break statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

         }

 

       } else if (stmt is ReturnStmt) {

-        if (specContextOnly) {

+        if (specContextOnly && !method.IsGhost) {

           Error(stmt, "return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

         }

       

@@ -1301,7 +1321,7 @@ namespace Microsoft.Dafny {
           if (var == null) {

             // the LHS didn't resolve correctly; some error would already have been reported

           } else {

-            lvalueIsGhost = var.IsGhost;

+            lvalueIsGhost = var.IsGhost || method.IsGhost;

             if (!var.IsMutable) {

               Error(stmt, "LHS of assignment must denote a mutable variable or field");

             }

@@ -1441,7 +1461,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

-        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);

+        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, method);

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

@@ -1473,11 +1493,16 @@ namespace Microsoft.Dafny {
           // any type is fine

         }

         s.IsGhost = bodyMustBeSpecOnly;

+        loopStack.Add(s);  // push

+        if (s.Labels == null) {  // otherwise, "s" is already in "inSpecOnlyContext" map

+          inSpecOnlyContext.Add(s, specContextOnly);

+        }

         ResolveStatement(s.Body, bodyMustBeSpecOnly, method);

+        loopStack.RemoveAt(loopStack.Count-1);  // pop

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

-        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);

+        s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, method);

         foreach (MaybeFreeExpression inv in s.Invariants) {

           ResolveExpression(inv.E, true);

           Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression

@@ -1643,7 +1668,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, Method method) {

+    bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {

       Contract.Requires(alternatives != null);

       Contract.Requires(method != null);

 

@@ -1661,6 +1686,13 @@ namespace Microsoft.Dafny {
           isGhost = isGhost || UsesSpecFeatures(alternative.Guard);

         }

       }

+

+      if (loopToCatchBreaks != null) {

+        loopStack.Add(loopToCatchBreaks);  // push

+        if (loopToCatchBreaks.Labels == null) {  // otherwise, "loopToCatchBreak" is already in "inSpecOnlyContext" map

+          inSpecOnlyContext.Add(loopToCatchBreaks, specContextOnly);

+        }

+      }

       foreach (var alternative in alternatives) {

         scope.PushMarker();

         foreach (Statement ss in alternative.Body) {

@@ -1668,6 +1700,10 @@ namespace Microsoft.Dafny {
         }

         scope.PopMarker();

       }

+      if (loopToCatchBreaks != null) {

+        loopStack.RemoveAt(loopStack.Count - 1);  // pop

+      }

+

       return isGhost;

     }

 

@@ -1795,25 +1831,33 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method)

     {

       Contract.Requires(blockStmt != null);

       Contract.Requires(method != null);

-      int labelsToPop = 0;

+

       foreach (Statement ss in blockStmt.Body) {

-        if (ss is LabelStmt) {

-          LabelStmt ls = (LabelStmt)ss;

-          labeledStatements.PushMarker();

-          bool b = labeledStatements.Push(ls.Label, ls);

-          Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed

-          labelsToPop++;

-        } else {

-          ResolveStatement(ss, specContextOnly, method);

-          for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }

+        labeledStatements.PushMarker();

+        // push labels

+        for (var lnode = ss.Labels; lnode != null; lnode = lnode.Next) {

+          Contract.Assert(lnode.Label != null);  // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet

+          var prev = labeledStatements.Find(lnode.Label);

+          if (prev == ss) {

+            Error(lnode.Tok, "duplicate label");

+          } else if (prev != null) {

+            Error(lnode.Tok, "label shadows an enclosing label");

+          } else {

+            bool b = labeledStatements.Push(lnode.Label, ss);

+            Contract.Assert(b);  // since we just checked for duplicates, we expect the Push to succeed

+            if (lnode == ss.Labels) {  // add it only once

+              inSpecOnlyContext.Add(ss, specContextOnly);

+            }

+          }

         }

+        ResolveStatement(ss, specContextOnly, method);

+        labeledStatements.PopMarker();

       }

-      for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }

     }

 

     Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, Method method) {

@@ -2544,25 +2588,43 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr.Type != null);  // this check approximates the requirement that "expr" be resolved

 

       if (expr is IdentifierExpr) {

-        IdentifierExpr e = (IdentifierExpr)expr;

+        var e = (IdentifierExpr)expr;

         if (e.Var != null && e.Var.IsGhost) {

           Error(expr, "ghost variables are allowed only in specification contexts");

           return;

         }

 

       } else if (expr is FieldSelectExpr) {

-        FieldSelectExpr e = (FieldSelectExpr)expr;

+        var e = (FieldSelectExpr)expr;

         if (e.Field != null && e.Field.IsGhost) {

           Error(expr, "ghost fields are allowed only in specification contexts");

           return;

         }

 

       } else if (expr is FunctionCallExpr) {

-        FunctionCallExpr e = (FunctionCallExpr)expr;

+        var e = (FunctionCallExpr)expr;

         if (e.Function != null && e.Function.IsGhost) {

           Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");

           return;

         }

+        // function is okay, so check all NON-ghost arguments

+        CheckIsNonGhost(e.Receiver);

+        for (int i = 0; i < e.Function.Formals.Count; i++) {

+          if (!e.Function.Formals[i].IsGhost) {

+            CheckIsNonGhost(e.Args[i]);

+          }

+        }

+        return;

+

+      } else if (expr is DatatypeValue) {

+        var e = (DatatypeValue)expr;

+        // check all NON-ghost arguments

+        for (int i = 0; i < e.Ctor.Formals.Count; i++) {

+          if (!e.Ctor.Formals[i].IsGhost) {

+            CheckIsNonGhost(e.Arguments[i]);

+          }

+        }

+        return;

 

       } else if (expr is OldExpr) {

         Error(expr, "old expressions are allowed only in specification and ghost contexts");

@@ -2577,7 +2639,7 @@ namespace Microsoft.Dafny {
         return;

 

       } else if (expr is BinaryExpr) {

-        BinaryExpr e = (BinaryExpr)expr;

+        var e = (BinaryExpr)expr;

         switch (e.ResolvedOp) {

           case BinaryExpr.ResolvedOpcode.RankGt:

           case BinaryExpr.ResolvedOpcode.RankLt:

@@ -2588,7 +2650,7 @@ namespace Microsoft.Dafny {
         }

 

       } else if (expr is QuantifierExpr) {

-        QuantifierExpr e = (QuantifierExpr)expr;

+        var e = (QuantifierExpr)expr;

         if (e.MissingBounds != null) {

           foreach (var bv in e.MissingBounds) {

             Error(expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

@@ -3454,7 +3516,7 @@ namespace Microsoft.Dafny {
         return Contract.Exists( me.Cases,mc=> UsesSpecFeatures(mc.Body));

       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

-        return UsesSpecFeatures(e.ResolvedExpression);

+        return e.ResolvedExpression != null && UsesSpecFeatures(e.ResolvedExpression);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index eb1d1cca..50e7965c 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -2899,7 +2899,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

       Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);

-

      

       return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);

     }

@@ -2912,7 +2911,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

       Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);

-

       

       TrStmt(block, builder, locals, etran);

       return builder.Collect(block.Tok);  // TODO: would be nice to have an end-curly location for "block"

@@ -2961,12 +2959,10 @@ namespace Microsoft.Dafny {
           }

         }

         

-      } else if (stmt is LabelStmt) {

-        AddComment(builder, stmt, "label statement");  // TODO: ouch, comments probably mess up what the label labels in the Boogie program

-        builder.AddLabelCmd(((LabelStmt)stmt).Label);

       } else if (stmt is BreakStmt) {

         AddComment(builder, stmt, "break statement");

-        builder.Add(new Bpl.BreakCmd(stmt.Tok, ((BreakStmt)stmt).TargetLabel));  // TODO: handle name clashes of labels

+        var s = (BreakStmt)stmt;

+        builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));

       } else if (stmt is ReturnStmt) {

         AddComment(builder, stmt, "return statement");

         builder.Add(new Bpl.ReturnCmd(stmt.Tok));

@@ -2988,6 +2984,9 @@ namespace Microsoft.Dafny {
       } else if (stmt is BlockStmt) {

         foreach (Statement ss in ((BlockStmt)stmt).Body) {

           TrStmt(ss, builder, locals, etran);

+          if (ss.Labels != null) {

+            builder.AddLabelCmd("after_" + ss.Labels.UniqueId);

+          }

         }

       } else if (stmt is IfStmt) {

         AddComment(builder, stmt, "if statement");

@@ -3259,7 +3258,7 @@ namespace Microsoft.Dafny {
       locals.Add(preLoopHeapVar);

       Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);

       ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);

-      builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));  // TODO: does this screw up labeled breaks for this loop?

+      builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));

 

       List<Bpl.Expr> initDecr = null;

       if (!Contract.Exists(theDecreases, e => e is WildcardExpr)) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index efcfa8bb..d997cba1 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -403,6 +403,22 @@ Dafny program verifier finished with 3 verified, 3 errors
 

 -------------------- ResolutionErrors.dfy --------------------

 ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context

+ResolutionErrors.dfy(100,9): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable

+ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context

+ResolutionErrors.dfy(144,16): Error: 'decreases *' is not allowed on ghost loops

+ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

+ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops

+ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

+ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

@@ -422,7 +438,9 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc
 ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

 ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

 ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

-20 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label

+ResolutionErrors.dfy(252,2): Error: duplicate label

+38 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

@@ -597,8 +615,120 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil
 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-

-Dafny program verifier finished with 15 verified, 6 errors

+ControlStructures.dfy(218,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    ControlStructures.dfy(197,3): anon62_LoopHead

+    (0,0): anon62_LoopBody

+    ControlStructures.dfy(197,3): anon63_Else

+    (0,0): anon3

+    ControlStructures.dfy(197,3): anon64_Else

+    (0,0): anon5

+    ControlStructures.dfy(201,5): anon65_LoopHead

+    (0,0): anon65_LoopBody

+    ControlStructures.dfy(201,5): anon66_Else

+    (0,0): anon8

+    ControlStructures.dfy(201,5): anon67_Else

+    (0,0): anon10

+    (0,0): anon71_Then

+    ControlStructures.dfy(213,9): anon72_LoopHead

+    (0,0): anon72_LoopBody

+    ControlStructures.dfy(213,9): anon73_Else

+    (0,0): anon20

+    (0,0): anon74_Then

+    (0,0): anon29

+ControlStructures.dfy(235,21): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    ControlStructures.dfy(197,3): anon62_LoopHead

+    (0,0): anon62_LoopBody

+    ControlStructures.dfy(197,3): anon63_Else

+    (0,0): anon3

+    ControlStructures.dfy(197,3): anon64_Else

+    (0,0): anon5

+    ControlStructures.dfy(201,5): anon65_LoopHead

+    (0,0): anon65_LoopBody

+    ControlStructures.dfy(201,5): anon66_Else

+    (0,0): anon8

+    ControlStructures.dfy(201,5): anon67_Else

+    (0,0): anon10

+    (0,0): anon71_Then

+    ControlStructures.dfy(213,9): anon72_LoopHead

+    (0,0): anon72_LoopBody

+    ControlStructures.dfy(213,9): anon73_Else

+    (0,0): anon20

+    ControlStructures.dfy(213,9): anon74_Else

+    (0,0): anon22

+    (0,0): anon75_Then

+    (0,0): after_4

+    ControlStructures.dfy(224,7): anon77_LoopHead

+    (0,0): anon77_LoopBody

+    ControlStructures.dfy(224,7): anon78_Else

+    (0,0): anon33

+    ControlStructures.dfy(224,7): anon79_Else

+    (0,0): anon35

+    (0,0): anon81_Then

+    (0,0): anon38

+    (0,0): after_9

+    (0,0): anon86_Then

+    (0,0): anon53

+ControlStructures.dfy(238,30): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    ControlStructures.dfy(197,3): anon62_LoopHead

+    (0,0): anon62_LoopBody

+    ControlStructures.dfy(197,3): anon63_Else

+    (0,0): anon3

+    ControlStructures.dfy(197,3): anon64_Else

+    (0,0): anon5

+    ControlStructures.dfy(201,5): anon65_LoopHead

+    (0,0): anon65_LoopBody

+    ControlStructures.dfy(201,5): anon66_Else

+    (0,0): anon8

+    ControlStructures.dfy(201,5): anon67_Else

+    (0,0): anon10

+    (0,0): anon68_Then

+    (0,0): after_5

+    (0,0): anon87_Then

+    (0,0): anon88_Then

+    (0,0): anon58

+ControlStructures.dfy(241,17): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    ControlStructures.dfy(197,3): anon62_LoopHead

+    (0,0): anon62_LoopBody

+    ControlStructures.dfy(197,3): anon63_Else

+    (0,0): anon3

+    ControlStructures.dfy(197,3): anon64_Else

+    (0,0): anon5

+    ControlStructures.dfy(201,5): anon65_LoopHead

+    (0,0): anon65_LoopBody

+    ControlStructures.dfy(201,5): anon66_Else

+    (0,0): anon8

+    ControlStructures.dfy(201,5): anon67_Else

+    (0,0): anon10

+    (0,0): anon71_Then

+    ControlStructures.dfy(213,9): anon72_LoopHead

+    (0,0): anon72_LoopBody

+    ControlStructures.dfy(213,9): anon73_Else

+    (0,0): anon20

+    ControlStructures.dfy(213,9): anon74_Else

+    (0,0): anon22

+    (0,0): anon75_Then

+    (0,0): after_4

+    ControlStructures.dfy(224,7): anon77_LoopHead

+    (0,0): anon77_LoopBody

+    ControlStructures.dfy(224,7): anon78_Else

+    (0,0): anon33

+    ControlStructures.dfy(224,7): anon79_Else

+    (0,0): anon35

+    (0,0): anon82_Then

+    (0,0): anon85_Then

+    (0,0): after_8

+    (0,0): anon89_Then

+    (0,0): anon61

+

+Dafny program verifier finished with 18 verified, 10 errors

 

 -------------------- Termination.dfy --------------------

 Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 2c9b3a35..5012e003 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -135,3 +135,108 @@ method B(x: int) returns (r: int)
       r := r - 1;

   }

 }

+

+// --------------- breaks ---------------

+

+method TheBreaker_AllGood(M: int, N: int, O: int)

+{

+  var a, b, c, d, e;

+  var i := 0;

+  while (i < M)

+  {

+    var j := 0;

+    label InnerHasLabel:

+    while (j < N)

+    {

+      var u := 2000;

+      label MyLabelBlock:

+      label MyLabelBlockAgain:

+      if (*) {

+        a := 15; break;

+      } else if (*) {

+        b := 12; break break;

+      } else if (*) {

+        c := 21; break InnerHasLabel;

+      } else if (*) {

+        while (u < 10000) {

+          u := u + 3;

+          if (*) { u := 1998; break MyLabelBlock; }

+          if (*) { u := 1998; break MyLabelBlockAgain; }

+        }

+        assert 10000 <= u;

+        u := 1998;

+      } else {

+        u := u - 2;

+      }

+      assert u == 1998;

+      var k := 0;

+      while

+        decreases O - k;

+      {

+        case k < O && k % 2 == 0 =>

+          d := 187; break;

+        case k < O =>

+          if (*) { e := 4; break InnerHasLabel; }

+          if (*) { e := 7; break; }

+          if (*) { e := 37; break break break; }

+          k := k + 1;

+      }

+      assert O <= k || d == 187 || e == 7;

+      j := j + 1;

+    }

+    assert N <= j || a == 15 || c == 21 || e == 4;

+    i := i + 1;

+  }

+  assert M <= i || b == 12 || e == 37;

+}

+

+method TheBreaker_SomeBad(M: int, N: int, O: int)

+{

+  var a, b, c, d, e;

+  var i := 0;

+  while (i < M)

+  {

+    var j := 0;

+    label InnerHasLabel:

+    while (j < N)

+    {

+      var u := 2000;

+      label MyLabelBlock:

+      label MyLabelBlockAgain:

+      if (*) {

+        a := 15; break;

+      } else if (*) {

+        b := 12; break break;

+      } else if (*) {

+        c := 21; break InnerHasLabel;

+      } else if (*) {

+        while (u < 10000) {

+          u := u + 3;

+          if (*) { u := 1998; break MyLabelBlock; }

+          if (*) { u := 1998; break MyLabelBlockAgain; }

+        }

+        assert u < 2000;  // error (and no way to get past this assert statement)

+      } else {

+        u := u - 2;

+      }

+      assert u == 1998;

+      var k := 0;

+      while

+        decreases O - k;

+      {

+        case k < O && k % 2 == 0 =>

+          d := 187; break;

+        case k < O =>

+          if (*) { e := 4; break InnerHasLabel; }

+          if (*) { e := 7; break; }

+          if (*) { e := 37; break break break; }

+          k := k + 1;

+      }

+      assert O <= k || e == 7;  // error: d == 187

+      j := j + 1;

+    }

+    assert N <= j || c == 21 || e == 4;  // error: a == 15

+    i := i + 1;

+  }

+  assert M <= i || b == 12;  // error: e == 37

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 56d7575f..09307b2b 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -87,3 +87,170 @@ method TestNameResolution1() {
   var e := Eleanor;

   assert Tuv(e, this.Eleanor) == 10;

 }

+

+// --------------- ghost tests -------------------------------------

+

+datatype GhostDt =

+  Nil(ghost extraInfo: int) |

+  Cons(data: int, tail: GhostDt, ghost moreInfo: int);

+

+class GhostTests {

+  method M(dt: GhostDt) returns (r: int) {

+    ghost var g := 5;

+    r := g;  // error: RHS is ghost, LHS is not

+    r := F(18, g);  // error: RHS is a ghost and will not be available at run time

+    r := G(20, g);  // it's fine to pass a ghost as a parameter to a non-ghost, because

+                    // only the ghost goes away during compilation

+    r := N(22, g);  // ditto

+    r := N(g, 22);  // error: passing in 'g' as non-ghost parameter

+    r := P(24, 22);  // error: 'P' is ghost, but its result is assigned to a non-ghost

+

+    match (dt) {

+      case Nil(gg) =>

+      case Cons(dd, tt, gg) =>

+        r := G(dd, dd);  // fine

+        r := G(dd, gg);  // fine

+        r := G(gg, gg);  // error: cannot pass ghost 'gg' as non-ghost parameter to 'G'

+    }

+    var dd;

+    dd := GhostDt.Nil(g);  // fine

+    dd := GhostDt.Cons(g, dt, 2);  // error: cannot pass 'g' as non-ghost parameter

+    ghost var dtg := GhostDt.Cons(g, dt, 2);  // fine, since result is ghost

+  }

+  function F(x: int, y: int): int {

+    y

+  }

+  function method G(x: int, ghost y: int): int {

+    y  // error: cannot return a ghost from a non-ghost function

+  }

+  function method H(dt: GhostDt): int {

+    match dt

+    case Nil(gg) =>  gg  // error: cannot return a ghost from a non-ghost function

+    case Cons(dd, tt, gg) =>  dd + gg  // error: ditto

+  }

+  method N(x: int, ghost y: int) returns (r: int) {

+    r := x;

+  }

+  ghost method P(x: int, y: int) returns (r: int) {

+    ghost var g := 5;

+    r := y;  // allowed, since the entire method is ghost

+    r := r + g;  // fine, for the same reason

+    r := N(20, 20);  // error: call to non-ghost method from ghost method is not okay

+  }

+  ghost method NiceTry()

+    ensures false;

+  {

+    while (true)

+      decreases *;  // error:  not allowed in ghost context

+    {

+    }

+  }

+  ghost method BreaksAreFineHere(t: int)

+  {

+    var n := 0;

+    ghost var k := 0;

+    while (true)

+      invariant n <= 112;

+      decreases 112 - n;

+    {

+      label MyStructure: {

+        if (k % 17 == 0) { break MyStructure; }  // this is fine, because it's a ghost method

+        k := k + 1;

+      }

+      label MyOtherStructure:

+      if (k % 17 == 0) {

+        break MyOtherStructure;

+      } else {

+        k := k + 1;

+      }

+

+      if (n == 112) {

+        break;

+      } else if (n == t) {

+        return;

+      }

+      n := n + 1;

+    }

+  }

+  method BreakMayNotBeFineHere(ghost t: int)

+  {

+    var n := 0;

+    ghost var k := 0;

+    var p := 0;

+    while (true)

+      invariant n <= 112;

+      decreases 112 - n;

+    {

+      label MyStructure: {

+        if (k % 17 == 0) { break MyStructure; }  // error: break from ghost to non-ghost point

+        k := k + 1;

+      }

+      label MyOtherStructure:

+      if (k % 17 == 0) {

+        break MyOtherStructure;  // this break is fine

+      } else {

+        k := k + 1;

+      }

+

+      var dontKnow;

+      if (n == 112) {

+        ghost var m := 0;

+        label LoopLabel0:

+        label LoopLabel1:

+        while (m < 200) {

+          if (m % 103 == 0) {

+            if {

+              case true => break;  // fine, since this breaks out of the enclosing ghost loop

+              case true => break LoopLabel0;  // fine

+              case true => break LoopLabel1;  // fine

+            }

+          } else if (m % 101 == 0) {

+            break break;  // error: break out of non-ghost loop from ghost context

+          }

+          m := m + 3;

+        }

+        break;

+      } else if (dontKnow == 708) {

+        var q := 0;

+        while (q < 1) {

+          label IfNest:

+          if (p == 67) {

+            break break;  // fine, since this is not a ghost context

+          } else if (*) {

+            break break break;  // error: tries to break out of more loop levels than there are

+          } else if (*) {

+            break break;  // fine, since this is not a ghost context

+          } else if (k == 67) {

+            break break;  // error, because this is a ghost context

+          }

+          q := q + 1;

+        }

+      } else if (n == t) {

+        return;  // error: this is a ghost context trying to return from a non-ghost method

+      }

+      n := n + 1;

+      p := p + 1;

+    }

+  }

+}

+

+method DuplicateLabels(n: int) {

+  var x;

+  if (n < 7) {

+    label DuplicateLabel: x := x + 1;

+  } else {

+    label DuplicateLabel: x := x + 1;

+  }

+  label DuplicateLabel: x := x + 1;

+  label DuplicateLabel: {

+    label AnotherLabel:

+    label DuplicateLabel:  // error: duplicate label

+    label OneMoreTime:

+    x := x + 1;

+  }

+  label DuplicateLabel:

+  label DuplicateLabel:  // error: duplicate label

+  x := x + 1;

+  label DuplicateLabel: x := x + 1;

+

+}

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index d3e0e82e..11c8c878 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -99,7 +99,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
   }

 }

 

-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)

+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)

   requires (forall a :: a in q ==> a < parent);

   ensures |SubstSeq(parent, q, v, val)| == |q|;

   ensures (forall k :: 0 <= k && k < |q| ==>