summaryrefslogtreecommitdiff
path: root/Source/Houdini/Houdini.cs
diff options
context:
space:
mode:
authorGravatar Ally Donaldson <unknown>2013-07-22 08:32:54 +0100
committerGravatar Ally Donaldson <unknown>2013-07-22 08:32:54 +0100
commit3b15454ac18f93e8f42913af80f665a900fd4378 (patch)
tree9716c10231d312c3e858d81bb3022c77432cb4ee /Source/Houdini/Houdini.cs
parentd65d530d398e1d1f742edc4b5fe16436df5a64e8 (diff)
Large refactoring of Hashtable to Dictionary.
Diffstat (limited to 'Source/Houdini/Houdini.cs')
-rw-r--r--Source/Houdini/Houdini.cs8
1 files changed, 4 insertions, 4 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index a91c0082..06d606ff 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,
@@ -1172,7 +1172,7 @@ namespace Microsoft.Boogie.Houdini {
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),
@@ -1192,7 +1192,7 @@ namespace Microsoft.Boogie.Houdini {
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),