From 438a12be8240dd425360704aab75089b329d36b6 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 5 Oct 2014 23:08:57 +0100
Subject: Fix bug in Duplicator where GotoCmd's LabelTargets and LabelNames
 where not updated during duplication to point to duplicated BasicBlocks.

Because the lists weren't being duplicated and resolved to the new basic blocks
a duplicated Implementation pointed into Blocks in the old implementation via
GotoCmds. This is bad and is not the expected behaviour.

Now if VisitImplementation() is called during duplication GotoCmds will be
resolved to point to duplicated Blocks.
---
 Source/Concurrency/OwickiGries.cs | 18 ------------------
 1 file changed, 18 deletions(-)

(limited to 'Source/Concurrency')

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 69e6b318..964bf024 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -19,7 +19,6 @@ namespace Microsoft.Boogie
         Implementation enclosingImpl;
         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */
         public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */
-        public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */
         public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */
         public HashSet<Procedure> yieldingProcs;
         public List<Implementation> impls;
@@ -32,7 +31,6 @@ namespace Microsoft.Boogie
             this.enclosingImpl = null;
             this.procMap = new Dictionary<Procedure, Procedure>();
             this.absyMap = new Dictionary<Absy, Absy>();
-            this.blockMap = new Dictionary<Block, Block>();
             this.implMap = new Dictionary<Implementation, Implementation>();
             this.yieldingProcs = new HashSet<Procedure>();
             this.impls = new List<Implementation>();
@@ -124,7 +122,6 @@ namespace Microsoft.Boogie
         public override Block VisitBlock(Block node)
         {
             Block block = base.VisitBlock(node);
-            blockMap[node] = block;
             absyMap[block] = node;
             return block;
         }
@@ -215,21 +212,6 @@ namespace Microsoft.Boogie
             implMap[impl] = node;
             impl.LocVars.Add(dummyLocalVar);
             impl.Name = impl.Proc.Name;
-            foreach (Block block in impl.Blocks)
-            {
-                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
-                if (gotoCmd == null) continue;
-                List<Block> labelTargets = new List<Block>();
-                List<string> labelNames = new List<string>();
-                foreach (Block x in gotoCmd.labelTargets)
-                {
-                    Block y = (Block)blockMap[x];
-                    labelTargets.Add(y);
-                    labelNames.Add(y.Label);
-                }
-                gotoCmd.labelTargets = labelTargets;
-                gotoCmd.labelNames = labelNames;
-            }
             return impl;
         }
 
-- 
cgit v1.2.3