Large refactoring of Hashtable to Dictionary.

12 files changed, 76 insertions, 76 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 5e69b179..520c6730 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -385,7 +385,7 @@ namespace Microsoft.Boogie {
 

       Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();

       Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();

-      Dictionary<Block/*!*/, Hashtable/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Hashtable/*!*/>();

+      Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>();

       Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>();

       Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>();

       Dictionary<Block, CallCmd> loopHeaderToCallCmd2 = new Dictionary<Block, CallCmd>();

@@ -402,7 +402,7 @@ namespace Microsoft.Boogie {
         IdentifierExprSeq callOutputs2 = new IdentifierExprSeq();

         List<AssignLhs> lhss = new List<AssignLhs>();

         List<Expr> rhss = new List<Expr>();

-        Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr

+        Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr

 

         VariableSeq/*!*/ targets = new VariableSeq();

         HashSet<Variable> footprint = new HashSet<Variable>();

@@ -2914,17 +2914,17 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private Hashtable/*Variable->Expr*//*?*/ formalMap = null;

+    private Dictionary<Variable, Expr>/*?*/ formalMap = null;

     public void ResetImplFormalMap() {

       this.formalMap = null;

     }

-    public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() {

+    public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {

       Contract.Ensures(Contract.Result<Hashtable>() != null);

 

       if (this.formalMap != null)

         return this.formalMap;

       else {

-        Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length);

+        Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Length + OutParams.Length);

 

         Contract.Assume(this.Proc != null);

         Contract.Assume(InParams.Length == Proc.InParams.Length);

@@ -2948,7 +2948,7 @@ namespace Microsoft.Boogie {
         if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

           Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name);

           using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, false)) {

-            foreach (DictionaryEntry e in map) {

+            foreach (var e in map) {

               Console.Write("  ");

               cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0);

               Console.Write("  --> ");

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 3005aaa6..cf6fa9ce 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2040,9 +2040,9 @@ namespace Microsoft.Boogie {
     protected override Cmd ComputeDesugaring() {

       Contract.Ensures(Contract.Result<Cmd>() != null);

       CmdSeq newBlockBody = new CmdSeq();

-      Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/();

-      Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();

-      Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/();

+      Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

+      Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();

+      Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();

       VariableSeq/*!*/ tempVars = new VariableSeq();

 

       // proc P(ins) returns (outs)

@@ -2335,7 +2335,7 @@ namespace Microsoft.Boogie {
 

   public class AssertCmd : PredicateCmd, IPotentialErrorNode {

     public Expr OrigExpr;

-    public Hashtable /*Variable -> Expr*/ IncarnationMap;

+    public Dictionary<Variable, Expr> IncarnationMap;

 

     // TODO: convert to use generics

     private object errorData;

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index fe189f83..d8b45d09 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -353,20 +353,20 @@ namespace Microsoft.Boogie {
   public delegate Expr/*?*/ Substitution(Variable/*!*/ v);

 

   public static class Substituter {

-    public static Substitution SubstitutionFromHashtable(Hashtable/*Variable!->Expr!*/ map) {

+    public static Substitution SubstitutionFromHashtable(Dictionary<Variable, Expr> map) {

       Contract.Requires(map != null);

       Contract.Ensures(Contract.Result<Substitution>() != null);

       // TODO: With Whidbey, could use anonymous functions.

       return new Substitution(new CreateSubstitutionClosure(map).Method);

     }

     private sealed class CreateSubstitutionClosure {

-      Hashtable/*Variable!->Expr!*//*!*/ map;

+      Dictionary<Variable /*!*/, Expr /*!*/>/*!*/ map;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(map != null);

       }

 

-      public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map)

+      public CreateSubstitutionClosure(Dictionary<Variable, Expr> map)

         : base() {

         Contract.Requires(map != null);

         this.map = map;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 57910775..b7626d99 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -328,7 +328,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(newModifies != null);

       Contract.Requires(newLocalVars != null);

       

-      Hashtable substMap = new Hashtable();

+      Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

       Procedure proc = impl.Proc;

 

       foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {

@@ -365,7 +365,7 @@ namespace Microsoft.Boogie {
         }

       }

 

-      Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();

+      Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();

 

       foreach (IdentifierExpr/*!*/ mie in proc.Modifies) {

         Contract.Assert(mie != null);

@@ -588,12 +588,12 @@ namespace Microsoft.Boogie {
     public Substitution Subst;

     public Substitution OldSubst;

 

-    public CodeCopier(Hashtable substMap) {

+    public CodeCopier(Dictionary<Variable, Expr> substMap) {

       Contract.Requires(substMap != null);

       Subst = Substituter.SubstitutionFromHashtable(substMap);

     }

 

-    public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) {

+    public CodeCopier(Dictionary<Variable, Expr> substMap, Dictionary<Variable, Expr> oldSubstMap) {

       Contract.Requires(oldSubstMap != null);

       Contract.Requires(substMap != null);

       Subst = Substituter.SubstitutionFromHashtable(substMap);

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index b3b02724..6874f1c9 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -95,7 +95,7 @@ namespace Microsoft.Boogie {
           Set freeVars = new Set();

           lambda.ComputeFreeVariables(freeVars);

           // this is ugly, the output will depend on hashing order

-          Hashtable subst = new Hashtable();

+          Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

           VariableSeq formals = new VariableSeq();

           ExprSeq callArgs = new ExprSeq();

           ExprSeq axCallArgs = new ExprSeq();

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index e353700f..63f9557f 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -281,7 +281,7 @@ namespace Microsoft.Boogie
             int count = 0;

             while (callCmd != null)

             {

-                Hashtable map = new Hashtable();

+                Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

                 foreach (Variable x in callCmd.Proc.InParams)

                 {

                     Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true);

@@ -317,7 +317,7 @@ namespace Microsoft.Boogie
             return proc;

         }

 

-        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Hashtable map)

+        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Dictionary<Variable, Expr> map)

         {

             if (yields.Count == 0) return;

 

@@ -354,8 +354,8 @@ namespace Microsoft.Boogie
                 locals.Add(copy);

                 map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);

             }

-            Hashtable ogOldLocalMap = new Hashtable();

-            Hashtable assumeMap = new Hashtable(map);

+            Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();

+            Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);

             foreach (IdentifierExpr ie in globalMods)

             {

                 Variable g = ie.Decl;

@@ -422,7 +422,7 @@ namespace Microsoft.Boogie
             Program program = linearTypechecker.program;

             ProcedureInfo info = procNameToInfo[impl.Name];

 

-            Hashtable map = new Hashtable();

+            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

             foreach (Variable local in impl.LocVars)

             {

                 var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));

@@ -717,7 +717,7 @@ namespace Microsoft.Boogie
                 yields.Add(cmds);

                 cmds = new CmdSeq();

             }

-            CreateYieldCheckerImpl(proc, yields, new Hashtable());

+            CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());

         }

 

         private void AddYieldProcAndImpl() 

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index 413cbf5b..341644ca 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -584,7 +584,7 @@ namespace VC {
     #region Program Passification

     private void GenerateHelperBlocks(Implementation impl) {

       Contract.Requires(impl != null);

-      Hashtable gotoCmdOrigins = new Hashtable();

+      Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();

       exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

       Contract.Assert(exitBlock != null);

 

@@ -622,7 +622,7 @@ namespace VC {
     }

 

 

-    private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {

+    private Dictionary<Variable, Expr> PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

       Contract.Requires(mvInfo != null);

       Contract.Requires(this.exitBlock != null);

@@ -744,14 +744,14 @@ namespace VC {
         ResetPredecessors(impl.Blocks);

         //EmitImpl(impl,false);

 

-        Hashtable/*Variable->Expr*/ htbl = PassifyProgram(impl, new ModelViewInfo(program, impl));

+        Dictionary<Variable, Expr> var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl));

 

         // Collect the last incarnation of each reachability variable in the passive program

         foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)

         {

-            if (htbl.ContainsKey(kvp.Value))

+            if (var2Expr.ContainsKey(kvp.Value))

             {

-                m_LastReachVarIncarnation[kvp.Value] = (Expr)htbl[kvp.Value];

+                m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value];

             }

         }

     }

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index a91c0082..06d606ff 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -264,7 +264,7 @@ namespace Microsoft.Boogie.Houdini {
       return newCmdSeq;

     }

     private CmdSeq InlineRequiresForCallCmd(CallCmd node) {

-      Hashtable substMap = new Hashtable();

+      Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

       for (int i = 0; i < node.Proc.InParams.Length; i++) {

         substMap.Add(node.Proc.InParams[i], node.Ins[i]);

       }

@@ -1149,7 +1149,7 @@ namespace Microsoft.Boogie.Houdini {
           if (assertCmd != null && MatchCandidate(assertCmd.Expr, out c)) {

             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

             if (currentHoudiniState.Assignment[cVar]) {

-              Hashtable cToTrue = new Hashtable();

+              Dictionary<Variable, Expr> cToTrue = new Dictionary<Variable, Expr>();

               Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

               cToTrue[cVarProg] = Expr.True;

               newCmds.Add(new AssumeCmd(assertCmd.tok,

@@ -1172,7 +1172,7 @@ namespace Microsoft.Boogie.Houdini {
             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

             if (currentHoudiniState.Assignment[cVar]) {

               Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

-              Hashtable subst = new Hashtable();

+              Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

               subst[cVarProg] = Expr.True;

               newRequires.Add(new Requires(Token.NoToken, true,

                 Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), r.Condition),

@@ -1192,7 +1192,7 @@ namespace Microsoft.Boogie.Houdini {
             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

             if (currentHoudiniState.Assignment[cVar]) {

               Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

-              Hashtable subst = new Hashtable();

+              Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

               subst[cVarProg] = Expr.True;

               newEnsures.Add(new Ensures(Token.NoToken, true,

                 Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), e.Condition),

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 7a738daf..edab3bf8 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -257,7 +257,7 @@ namespace Microsoft.Boogie {
         var s = states[i];

         if (0 <= s && s < MvInfo.CapturePoints.Count) {

           VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];

-          var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable();

+          var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Dictionary<Variable, Expr>();

           var cs = m.MkState(map.Description);

 

           foreach (Variable v in MvInfo.AllVariables) {

@@ -756,7 +756,7 @@ namespace VC {
     /// already been constructed for the implementation (and so

     /// is already an element of impl.Blocks)

     /// </param>

-    protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins) {

+    protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {

       Contract.Requires(impl != null);

       Contract.Requires(unifiedExitBlock != null);

       Contract.Requires(gotoCmdOrigins != null);

@@ -1085,7 +1085,7 @@ namespace VC {
     }

 

 

-    protected Block GenerateUnifiedExit(Implementation impl, Hashtable gotoCmdOrigins) {

+    protected Block GenerateUnifiedExit(Implementation impl, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {

       Contract.Requires(impl != null);

       Contract.Requires(gotoCmdOrigins != null);

       Contract.Ensures(Contract.Result<Block>() != null);

@@ -1112,7 +1112,7 @@ namespace VC {
               BlockSeq bs = new BlockSeq();

               bs.Add(unifiedExit);

               GotoCmd go = new GotoCmd(Token.NoToken, labels, bs);

-              gotoCmdOrigins[go] = b.TransferCmd;

+              gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd;

               b.TransferCmd = go;

               unifiedExit.Predecessors.Add(b);

             }

@@ -1187,31 +1187,31 @@ namespace VC {
     /// <param name="b"></param>

     /// <param name="block2Incarnation">Gives incarnation maps for b's predecessors.</param>

     /// <returns></returns>

-    protected Hashtable /*Variable -> Expr*/ ComputeIncarnationMap(Block b, Hashtable /*Variable -> Expr*/ block2Incarnation) {

+    protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b, Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation) {

       Contract.Requires(b != null);

       Contract.Requires(block2Incarnation != null);

       Contract.Ensures(Contract.Result<Hashtable>() != null);

 

       if (b.Predecessors.Length == 0) {

-        return new Hashtable();

+        return new Dictionary<Variable, Expr>();

       }

 

-      Hashtable /*Variable -> Expr*/ incarnationMap = null;

+      Dictionary<Variable, Expr> incarnationMap = null;

       Set /*Variable*/ fixUps = new Set /*Variable*/ ();

       foreach (Block pred in b.Predecessors) {

         Contract.Assert(pred != null);

-        Contract.Assert(block2Incarnation.Contains(pred));  // otherwise, Passive Transformation found a block whose predecessors have not been processed yet

-        Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)block2Incarnation[pred];

+        Contract.Assert(block2Incarnation.ContainsKey(pred));  // otherwise, Passive Transformation found a block whose predecessors have not been processed yet

+        Dictionary<Variable, Expr> predMap = (Dictionary<Variable, Expr>)block2Incarnation[pred];

         Contract.Assert(predMap != null);

         if (incarnationMap == null) {

-          incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone();

+          incarnationMap = new Dictionary<Variable, Expr>(predMap);

           continue;

         }

 

         ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ ();

         foreach (Variable v in incarnationMap.Keys) {

           Contract.Assert(v != null);

-          if (!predMap.Contains(v)) {

+          if (!predMap.ContainsKey(v)) {

             // conflict!!

             conflicts.Add(v);

             fixUps.Add(v);

@@ -1224,7 +1224,7 @@ namespace VC {
         }

         foreach (Variable v in predMap.Keys) {

           Contract.Assert(v != null);

-          if (!incarnationMap.Contains(v)) {

+          if (!incarnationMap.ContainsKey(v)) {

             // v was not in the domain of the predecessors seen so far, so it needs to be fixed up

             fixUps.Add(v);

           } else {

@@ -1251,7 +1251,7 @@ namespace VC {
           Contract.Assert(pred != null);

           #region Create an assume command equating v_prime with its last incarnation in pred

           #region Create an identifier expression for the last incarnation in pred

-          Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]);

+          Dictionary<Variable, Expr> predMap = (Dictionary<Variable, Expr>)cce.NonNull(block2Incarnation[pred]);

 

           Expr pred_incarnation_exp;

           Expr o = (Expr)predMap[v];

@@ -1279,9 +1279,9 @@ namespace VC {
       return incarnationMap;

     }

 

-    Hashtable preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

+    Dictionary<Variable, Expr> preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

 

-    protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {

+    protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {

       Contract.Requires(b != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(mvInfo != null);

@@ -1304,11 +1304,11 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {

+    protected Dictionary<Variable, Expr> Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

       Contract.Requires(mvInfo != null);

 

-      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

+      Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

 

       RestoreParamWhereClauses(impl);

 

@@ -1322,7 +1322,7 @@ namespace VC {
       return r;

     }

 

-    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

+    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

       Contract.Requires(blocks != null);

       Contract.Requires(modifies != null);

       Contract.Requires(mvInfo != null);

@@ -1349,13 +1349,13 @@ namespace VC {
 

       // Now we can process the nodes in an order so that we're guaranteed to have

       // processed all of a node's predecessors before we process the node.

-      Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

+      Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation = new Dictionary<Block, Dictionary<Variable, Expr>>();

       Block exitBlock = null;

-      Hashtable exitIncarnationMap = null;

+      Dictionary<Variable, Expr> exitIncarnationMap = null;

       foreach (Block b in sortedNodes) {

         Contract.Assert(b != null);

-        Contract.Assert(!block2Incarnation.Contains(b));

-        Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

+        Contract.Assert(!block2Incarnation.ContainsKey(b));

+        Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

 

         // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.

         b.liveVarsBefore = null;

@@ -1398,11 +1398,11 @@ namespace VC {
     /// </summary>

     protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)

     {

-      Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();

+      Dictionary<Variable, Expr> oldFrameMap = new Dictionary<Variable, Expr>();

       foreach (IdentifierExpr ie in modifies)

       {

         Contract.Assert(ie != null);

-        if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))

+        if (!oldFrameMap.ContainsKey(cce.NonNull(ie.Decl)))

           oldFrameMap.Add(ie.Decl, ie);

       }

       return Substituter.SubstitutionFromHashtable(oldFrameMap);

@@ -1412,7 +1412,7 @@ namespace VC {
     /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc

     /// Meanwhile, record any information needed to later reconstruct a model view.

     /// </summary>

-    protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {

+    protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {

       Contract.Requires(c != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(oldFrameSubst != null);

@@ -1432,14 +1432,14 @@ namespace VC {
           if (description != null) {

             Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));

             copy = Bpl.Expr.And(mv, copy);

-            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone()));

+            mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap)));

           }

         }

         Contract.Assert(copy != null);

         if (pc is AssertCmd) {

           ((AssertCmd)pc).OrigExpr = pc.Expr;

           Contract.Assert(((AssertCmd)pc).IncarnationMap == null);

-          ((AssertCmd)pc).IncarnationMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(incarnationMap.Clone());

+          ((AssertCmd)pc).IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

         }

         pc.Expr = copy;

         passiveCmds.Add(pc);

@@ -1518,7 +1518,7 @@ namespace VC {
       #region havoc w |--> assume whereClauses, out := in( w |-> w' )

  else if (c is HavocCmd) {

         if (this.preHavocIncarnationMap == null)      // Save a copy of the incarnation map (at the top of a sequence of havoc statements)

-          this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();

+          this.preHavocIncarnationMap = new Dictionary<Variable, Expr>(incarnationMap);

 

         HavocCmd hc = (HavocCmd)c;

         Contract.Assert(c != null);

@@ -1748,8 +1748,8 @@ namespace VC {
     public class Mapping

     {

       public readonly string Description;

-      public readonly Hashtable /*Variable -> Expr*/ IncarnationMap;

-      public Mapping(string description, Hashtable /*Variable -> Expr*/ incarnationMap) {

+      public readonly Dictionary<Variable, Expr> IncarnationMap;

+      public Mapping(string description, Dictionary<Variable, Expr> incarnationMap) {

         Description = description;

         IncarnationMap = incarnationMap;

       }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 7b20622a..78ed8cb5 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -1871,7 +1871,7 @@ namespace Microsoft.Boogie
                 Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);

                 VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];

                 var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)

-                  ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

+                  ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();

                 var cs = m.MkState(map.Description);

 

                 foreach (Variable v in info.AllVariables)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 4078b43e..01b34504 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2472,7 +2472,7 @@ namespace VC {
           Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);

           VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];

           var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)

-            ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

+            ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();

           var cs = m.MkState(map.Description);

 

           foreach (Variable v in info.AllVariables) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bc83e529..bf2bf324 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -531,7 +531,7 @@ namespace VC {
       double total_cost;

       int assertion_count;

       double assertion_cost; // without multiplication by paths

-      Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;

+      Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;

       readonly public VCGen/*!*/ parent;

       Implementation/*!*/ impl;

 

@@ -548,7 +548,7 @@ namespace VC {
       private int splitNo;

       internal ErrorReporter reporter;

 

-      public Split(List<Block/*!*/>/*!*/ blocks, Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {

+      public Split(List<Block/*!*/>/*!*/ blocks, Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {

         Contract.Requires(cce.NonNullElements(blocks));

         Contract.Requires(gotoCmdOrigins != null);

         Contract.Requires(par != null);

@@ -974,13 +974,13 @@ namespace VC {
         copies.Clear();

         CloneBlock(blocks[0]);

         List<Block> newBlocks = new List<Block>();

-        Hashtable newGotoCmdOrigins = new Hashtable();

+        Dictionary<TransferCmd, ReturnCmd> newGotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();

         foreach (Block b in blocks) {

           Contract.Assert(b != null);

           Block tmp;

           if (copies.TryGetValue(b, out tmp)) {

             newBlocks.Add(cce.NonNull(tmp));

-            if (gotoCmdOrigins.ContainsKey(b)) {

+            if (gotoCmdOrigins.ContainsKey(b.TransferCmd)) {

               newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd];

             }

 

@@ -1235,7 +1235,7 @@ namespace VC {
 

             ResetPredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

+            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

             int ac;  // computed, but then ignored for this CodeExpr

             VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

             VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

@@ -1653,7 +1653,7 @@ namespace VC {
     }

 

     public class ErrorReporter : ProverInterface.ErrorHandler {

-      Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;

+      Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;

       Dictionary<int, Absy>/*!*/ label2absy;

       List<Block/*!*/>/*!*/ blocks;

       protected Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap;

@@ -1686,7 +1686,7 @@ namespace VC {
       protected ProverContext/*!*/ context;

       Program/*!*/ program;

 

-      public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,

+      public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,

           Dictionary<int, Absy>/*!*/ label2absy,

           List<Block/*!*/>/*!*/ blocks,

           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

@@ -1782,7 +1782,7 @@ namespace VC {
     }

 

     public class ErrorReporterLocal : ErrorReporter {

-      public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,

+      public ErrorReporterLocal(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,

           Dictionary<int, Absy>/*!*/ label2absy,

           List<Block/*!*/>/*!*/ blocks,

           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

@@ -2097,13 +2097,13 @@ namespace VC {
       }

     }

 

-    public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

+    public Dictionary<TransferCmd, ReturnCmd> PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

       Contract.Ensures(Contract.Result<Hashtable>() != null);

 

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();

+      Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();

       Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

       

       #region Debug Tracing

@@ -2216,7 +2216,7 @@ namespace VC {
           cmds.AddRange(entryBlock.Cmds);

           entryBlock.Cmds = cmds;

           // Make sure that all added commands are passive commands.

-          Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());

+          Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary<Block, Dictionary<Variable, Expr>>());

           TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,

                                ComputeOldExpressionSubstitution(impl.Proc.Modifies));

         }