merge

4 files changed, 13 insertions, 13 deletions

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 24a3c708..2ff5975e 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -565,7 +565,7 @@ namespace Microsoft.Boogie.Houdini {
         private void GenVC(Implementation impl)

         {

             ModelViewInfo mvInfo;

-            System.Collections.Hashtable label2absy;

+            Dictionary<int, Absy> label2absy;

             var collector = new AbsHoudiniCounterexampleCollector(this);

             collector.OnProgress("HdnVCGen", 0, 0, 0.0);

 

@@ -2238,7 +2238,7 @@ namespace Microsoft.Boogie.Houdini {
 

             foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())

             {

-                var nensures = new EnsuresSeq();

+                var nensures = new List<Ensures>();

                 proc.Ensures.OfType<Ensures>()

                 .Where(ens => !QKeyValue.FindBoolAttribute(ens.Attributes, "ah") &&

                     !QKeyValue.FindBoolAttribute(ens.Attributes, "pre") &&

@@ -2792,7 +2792,7 @@ namespace Microsoft.Boogie.Houdini {
         private void GenVC(Implementation impl)

         {

             ModelViewInfo mvInfo;

-            System.Collections.Hashtable label2absy;

+            Dictionary<int, Absy> label2absy;

 

             if (CommandLineOptions.Clo.Trace)

             {

@@ -3147,7 +3147,7 @@ namespace Microsoft.Boogie.Houdini {
                 PosPrePreds[impl.Name].UnionWith(posPreT);

 

                 // Pick up per-procedure pre-post

-                var nens = new EnsuresSeq();

+                var nens = new List<Ensures>();

                 foreach (var ens in impl.Proc.Ensures.OfType<Ensures>())

                 {

                     string s = null;

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index 9a2eb404..0f725ccf 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -437,7 +437,7 @@ namespace Microsoft.Boogie.Houdini {
         {

 

           #region Handle the preconditions

-          RequiresSeq newRequires = new RequiresSeq();

+          List<Requires> newRequires = new List<Requires>();

           foreach(Requires r in p.Requires) {

             string c;

             if (Houdini.MatchCandidate(r.Condition, candidates, out c)) {

@@ -457,7 +457,7 @@ namespace Microsoft.Boogie.Houdini {
           #endregion

 

           #region Handle the postconditions

-          EnsuresSeq newEnsures = new EnsuresSeq();

+          List<Ensures> newEnsures = new List<Ensures>();

           foreach(Ensures e in p.Ensures) {

             string c;

             if (Houdini.MatchCandidate(e.Condition, candidates, out c)) {

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index b29aa933..ce46f20b 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -155,7 +155,7 @@ namespace Microsoft.Boogie.Houdini {
       var exprGen = proverInterface.Context.ExprGen;

       VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

 

-      Hashtable/*<int, Absy!>*/ label2absy;

+      Dictionary<int, Absy> label2absy;

       conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context);

       if (!CommandLineOptions.Clo.UseLabels) {

         VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index a91c0082..5078d5a5 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,

@@ -1165,14 +1165,14 @@ namespace Microsoft.Boogie.Houdini {
       }

 

       foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

-        RequiresSeq newRequires = new RequiresSeq();

+        List<Requires> newRequires = new List<Requires>();

         foreach (Requires r in proc.Requires) {

           string c;

           if (MatchCandidate(r.Condition, out c)) {

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

@@ -1185,14 +1185,14 @@ namespace Microsoft.Boogie.Houdini {
         }

         proc.Requires = newRequires;

 

-        EnsuresSeq newEnsures = new EnsuresSeq();

+        List<Ensures> newEnsures = new List<Ensures>();

         foreach (Ensures e in proc.Ensures) {

           string c;

           if (MatchCandidate(e.Condition, out c)) {

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