From 49e3076cd0fa9a11f8df94f1e40e28045125b8de Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 7 Mar 2012 13:13:22 -0800
Subject: Dafny: added ghost modules (the meaning is simply that such a module
 will not be compiled) Dafny: improved :autocontracts heuristic for detecting
 "simple query method" Dafny: fixed some bugs

---
 Source/Dafny/RefinementTransformer.cs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index c37ba18f..36ae8f22 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -494,7 +494,11 @@ namespace Microsoft.Dafny {
     void AddStmtLabels(Statement s, LabelNode node) {
       if (node != null) {
         AddStmtLabels(s, node.Next);
-        s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);
+        if (node.Label == null) {
+          // this indicates an implicit-target break statement that has been resolved; don't add it
+        } else {
+          s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);
+        }
       }
     }
 
-- 
cgit v1.2.3