From 717acb3230145241f08f7d6f7cb2a68fe1f257e8 Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 22 Jul 2013 07:45:14 +0100
Subject: Refactored labsl2absy so that it is a Dictionary<int, Absy> instead
 of a plain Hashtable.

---
 Source/Doomed/DoomCheck.cs        | 18 +++++++++---------
 Source/Doomed/DoomErrorHandler.cs |  4 ++--
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'Source/Doomed')

diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index b317dc71..6b9f91cf 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -151,7 +151,7 @@ void ObjectInvariant()
         }
 
         #region Attributes
-        public Hashtable Label2Absy;
+        public Dictionary<int, Absy> Label2Absy;
         public DoomErrorHandler ErrorHandler {
             set {
                 m_ErrHandler = value;
@@ -219,9 +219,9 @@ void ObjectInvariant()
                     
             }
 
-            Label2Absy = new Hashtable(); // This is only a dummy
+            Label2Absy = new Dictionary<int, Absy>(); // This is only a dummy
             m_Evc = new Evc(check);
-            Hashtable l2a = null;
+            Dictionary<int, Absy> l2a = null;
             VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
             Contract.Assert(vce != null);
             Contract.Assert( l2a!=null);
@@ -235,9 +235,9 @@ void ObjectInvariant()
         {
             Contract.Requires(check != null);
             m_Check = check;
-            Label2Absy = new Hashtable(); // This is only a dummy
+            Label2Absy = new Dictionary<int, Absy>(); // This is only a dummy
             m_Evc = new Evc(check);
-            Hashtable l2a = null;
+            Dictionary<int, Absy> l2a = null;
             int assertionCount;  // compute and then ignore
             VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
             Contract.Assert(vce != null);
@@ -301,14 +301,14 @@ void ObjectInvariant()
 
        */
 
-        VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) {
+        VCExpr GenerateEVC(Implementation impl, out Dictionary<int, Absy> label2absy, Checker ch, out int assertionCount) {
           Contract.Requires(impl != null);
           Contract.Requires(ch != null);
           Contract.Ensures(Contract.Result<VCExpr>() != null);
 
           TypecheckingContext tc = new TypecheckingContext(null);
           impl.Typecheck(tc);
-          label2absy = new Hashtable/*<int, Absy!>*/();
+          label2absy = new Dictionary<int, Absy>();
           VCExpr vc;
           switch (CommandLineOptions.Clo.vcVariety) {
             case CommandLineOptions.VCVariety.Doomed:
@@ -322,7 +322,7 @@ void ObjectInvariant()
         }
 
         public VCExpr LetVC(Block startBlock,
-                            Hashtable/*<int, Absy!>*/ label2absy,
+                            Dictionary<int, Absy> label2absy,
                             ProverContext proverCtxt,
                             out int assertionCount)
         {
@@ -342,7 +342,7 @@ void ObjectInvariant()
         }
 
         VCExpr LetVC(Block block,
-                     Hashtable/*<int, Absy!>*/ label2absy,
+                     Dictionary<int, Absy> label2absy,
                      Hashtable/*<Block, VCExprVar!>*/ blockVariables,
                      List<VCExprLetBinding> bindings,
                      ProverContext proverCtxt,
diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs
index 33d8b68e..a85adbe1 100644
--- a/Source/Doomed/DoomErrorHandler.cs
+++ b/Source/Doomed/DoomErrorHandler.cs
@@ -15,7 +15,7 @@ namespace VC
     internal class DoomErrorHandler : ProverInterface.ErrorHandler
     {
 
-        protected Hashtable label2Absy;
+        protected Dictionary<int, Absy> label2Absy;
         protected VerifierCallback callback;
         private List<Block> m_CurrentTrace = new List<Block>();
 
@@ -28,7 +28,7 @@ namespace VC
         }
 
 
-        public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback)
+        public DoomErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback)
         {
             Contract.Requires(label2Absy != null);
             Contract.Requires(callback != null);
-- 
cgit v1.2.3