diff options
-rw-r--r-- | Source/Doomed/VCDoomed.cs | 2 | ||||
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 4 | ||||
-rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 2 | ||||
-rw-r--r-- | Source/VCGeneration/VC.cs | 4 |
4 files changed, 6 insertions, 6 deletions
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 778ae767..413cbf5b 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -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;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index f625de75..7a738daf 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -578,7 +578,7 @@ namespace VC { protected VariableSeq CurrentLocalVariables = null;
// shared across each implementation; created anew for each implementation
- protected Hashtable /*Variable -> int*/ variable2SequenceNumber;
+ protected Dictionary<Variable, int> variable2SequenceNumber;
public Dictionary<Incarnation, Absy>/*!>!*/ incarnationOriginMap = new Dictionary<Incarnation, Absy>();
public Program program;
@@ -1162,7 +1162,7 @@ namespace VC { int currentIncarnationNumber =
variable2SequenceNumber.ContainsKey(x)
?
- (int)cce.NonNull(variable2SequenceNumber[x])
+ variable2SequenceNumber[x]
:
-1;
Variable v = new Incarnation(x, currentIncarnationNumber + 1);
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index cf33c53e..7b20622a 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -126,7 +126,7 @@ namespace Microsoft.Boogie Contract.Requires(impl != null);
CurrentLocalVariables = impl.LocVars;
- variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ variable2SequenceNumber = new Dictionary<Variable, int>();
incarnationOriginMap = new Dictionary<Incarnation, Absy>();
ResetPredecessors(impl.Blocks);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index af3454f5..cfc7955b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1228,7 +1228,7 @@ namespace VC { delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)
{
VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
- vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
vcgen.CurrentLocalVariables = codeExpr.LocVars;
// codeExpr.Blocks.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
@@ -1861,7 +1861,7 @@ namespace VC { impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
CurrentLocalVariables = impl.LocVars;
- variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ variable2SequenceNumber = new Dictionary<Variable, int>();
incarnationOriginMap = new Dictionary<Incarnation, Absy>();
#region Debug Tracing
|