Refactored variable2sequenceNumber to use Dictionary

4 files changed, 6 insertions, 6 deletions

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index 778ae767..413cbf5b 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -692,7 +692,7 @@ namespace VC {
 

     private void Transform4DoomedCheck(Implementation impl)

     {

-        variable2SequenceNumber = new Hashtable/*Variable -> int*/();

+        variable2SequenceNumber = new Dictionary<Variable, int>();

         incarnationOriginMap = new Dictionary<Incarnation, Absy>();

         if (impl.Blocks.Count < 1) return;

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index f625de75..7a738daf 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -578,7 +578,7 @@ namespace VC {
     protected VariableSeq CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

-    protected Hashtable /*Variable -> int*/ variable2SequenceNumber;

+    protected Dictionary<Variable, int> variable2SequenceNumber;

     public Dictionary<Incarnation, Absy>/*!>!*/ incarnationOriginMap = new Dictionary<Incarnation, Absy>();

 

     public Program program;

@@ -1162,7 +1162,7 @@ namespace VC {
       int currentIncarnationNumber =

         variable2SequenceNumber.ContainsKey(x)

         ?

-        (int)cce.NonNull(variable2SequenceNumber[x])

+        variable2SequenceNumber[x]

         :

         -1;

       Variable v = new Incarnation(x, currentIncarnationNumber + 1);

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index cf33c53e..7b20622a 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -126,7 +126,7 @@ namespace Microsoft.Boogie
             Contract.Requires(impl != null);

 

             CurrentLocalVariables = impl.LocVars;

-            variable2SequenceNumber = new Hashtable/*Variable -> int*/();

+            variable2SequenceNumber = new Dictionary<Variable, int>();

             incarnationOriginMap = new Dictionary<Incarnation, Absy>();

 

             ResetPredecessors(impl.Blocks);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index af3454f5..cfc7955b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1228,7 +1228,7 @@ namespace VC {
           delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)

           {

             VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);

-            vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();

+            vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();

             vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

             vcgen.CurrentLocalVariables = codeExpr.LocVars;

             // codeExpr.Blocks.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -1861,7 +1861,7 @@ namespace VC {
       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

 

       CurrentLocalVariables = impl.LocVars;

-      variable2SequenceNumber = new Hashtable/*Variable -> int*/();

+      variable2SequenceNumber = new Dictionary<Variable, int>();

       incarnationOriginMap = new Dictionary<Incarnation, Absy>();

 

       #region Debug Tracing