merge

3 files changed, 17 insertions, 17 deletions

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);

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index 778ae767..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);

@@ -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;

 

@@ -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];

             }

         }

     }