From c6d9da6f688c18844c7f6a471030cce513e848b0 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 26 May 2011 23:40:33 -0700
Subject: 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

---
 Source/Dafny/Printer.cs | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'Source/Dafny/Printer.cs')

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index f5fba723..c92b477a 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/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) {
-- 
cgit v1.2.3