From 43391b50592e2c484872845ff05d670c571f659d Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Wed, 6 Jun 2012 15:54:48 -0700
Subject: Dafny: change labels to use a generic singly linked list

---
 Dafny/Resolver.cs | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'Dafny/Resolver.cs')

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 7be3fca2..23cf892e 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1355,7 +1355,7 @@ namespace Microsoft.Dafny {
             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);
+              target.Labels = new LList<Label>(new Label(target.Tok, null), null);
             }
             s.TargetStmt = target;
             if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {
@@ -2158,17 +2158,18 @@ namespace Microsoft.Dafny {
       foreach (Statement ss in blockStmt.Body) {
         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);
+        for (var l = ss.Labels; l != null; l = l.Next) {
+          var lnode = l.Data;
+          Contract.Assert(lnode.Name != 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.Name);
           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);
+            bool b = labeledStatements.Push(lnode.Name, ss);
             Contract.Assert(b);  // since we just checked for duplicates, we expect the Push to succeed
-            if (lnode == ss.Labels) {  // add it only once
+            if (l == ss.Labels) {  // add it only once
               inSpecOnlyContext.Add(ss, specContextOnly);
             }
           }
-- 
cgit v1.2.3