Fixed bugs arising from differences between hashtables and dictionaries

3 files changed, 9 insertions, 5 deletions

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index d8b45d09..1bea5880 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -373,7 +373,10 @@ namespace Microsoft.Boogie {
       }

       public Expr/*?*/ Method(Variable v) {

         Contract.Requires(v != null);

-        return (Expr)map[v];

+        if(map.ContainsKey(v)) {

+          return map[v];

+        }

+        return null;

       }

     }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index edab3bf8..202557ff 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -261,10 +261,11 @@ namespace Microsoft.Boogie {
           var cs = m.MkState(map.Description);

 

           foreach (Variable v in MvInfo.AllVariables) {

-            var e = (Expr)map.IncarnationMap[v];

+            Expr e = map.IncarnationMap.ContainsKey(v) ? map.IncarnationMap[v] : null;

             if (e == null) continue;

 

-            if (prevInc[v] == e) continue; // skip unchanged variables

+            Expr prevIncV = prevInc.ContainsKey(v) ? prevInc[v] : null;

+            if (prevIncV == e) continue; // skip unchanged variables

 

             Model.Element elt;

 

@@ -1254,7 +1255,7 @@ namespace VC {
           Dictionary<Variable, Expr> predMap = (Dictionary<Variable, Expr>)cce.NonNull(block2Incarnation[pred]);

 

           Expr pred_incarnation_exp;

-          Expr o = (Expr)predMap[v];

+          Expr o = predMap.ContainsKey(v) ? predMap[v] : null;

           if (o == null) {

             Variable predIncarnation = v;

             IdentifierExpr ie2 = new IdentifierExpr(predIncarnation.tok, predIncarnation);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bf2bf324..09874382 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1751,7 +1751,7 @@ namespace VC {
           foreach (Block b in returnExample.Trace) {

             Contract.Assert(b != null);

             Contract.Assume(b.TransferCmd != null);

-            ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];

+            ReturnCmd cmd = gotoCmdOrigins.ContainsKey(b.TransferCmd) ? gotoCmdOrigins[b.TransferCmd] : null;

             if (cmd != null) {

               returnExample.FailingReturn = cmd;

               break;