diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 12 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 8 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 6 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 8 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 2 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 12 |
6 files changed, 24 insertions, 24 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 5e69b179..520c6730 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -385,7 +385,7 @@ namespace Microsoft.Boogie { Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
- Dictionary<Block/*!*/, Hashtable/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Hashtable/*!*/>();
+ Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>();
Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>();
Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>();
Dictionary<Block, CallCmd> loopHeaderToCallCmd2 = new Dictionary<Block, CallCmd>();
@@ -402,7 +402,7 @@ namespace Microsoft.Boogie { IdentifierExprSeq callOutputs2 = new IdentifierExprSeq();
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
- Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr
+ Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr
VariableSeq/*!*/ targets = new VariableSeq();
HashSet<Variable> footprint = new HashSet<Variable>();
@@ -2914,17 +2914,17 @@ namespace Microsoft.Boogie { }
}
- private Hashtable/*Variable->Expr*//*?*/ formalMap = null;
+ private Dictionary<Variable, Expr>/*?*/ formalMap = null;
public void ResetImplFormalMap() {
this.formalMap = null;
}
- public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() {
+ public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {
Contract.Ensures(Contract.Result<Hashtable>() != null);
if (this.formalMap != null)
return this.formalMap;
else {
- Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length);
+ Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Length + OutParams.Length);
Contract.Assume(this.Proc != null);
Contract.Assume(InParams.Length == Proc.InParams.Length);
@@ -2948,7 +2948,7 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name);
using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, false)) {
- foreach (DictionaryEntry e in map) {
+ foreach (var e in map) {
Console.Write(" ");
cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0);
Console.Write(" --> ");
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 3005aaa6..cf6fa9ce 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2040,9 +2040,9 @@ namespace Microsoft.Boogie { protected override Cmd ComputeDesugaring() {
Contract.Ensures(Contract.Result<Cmd>() != null);
CmdSeq newBlockBody = new CmdSeq();
- Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/();
- Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();
- Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/();
+ Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();
VariableSeq/*!*/ tempVars = new VariableSeq();
// proc P(ins) returns (outs)
@@ -2335,7 +2335,7 @@ namespace Microsoft.Boogie { public class AssertCmd : PredicateCmd, IPotentialErrorNode {
public Expr OrigExpr;
- public Hashtable /*Variable -> Expr*/ IncarnationMap;
+ public Dictionary<Variable, Expr> IncarnationMap;
// TODO: convert to use generics
private object errorData;
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index fe189f83..d8b45d09 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -353,20 +353,20 @@ namespace Microsoft.Boogie { public delegate Expr/*?*/ Substitution(Variable/*!*/ v);
public static class Substituter {
- public static Substitution SubstitutionFromHashtable(Hashtable/*Variable!->Expr!*/ map) {
+ public static Substitution SubstitutionFromHashtable(Dictionary<Variable, Expr> map) {
Contract.Requires(map != null);
Contract.Ensures(Contract.Result<Substitution>() != null);
// TODO: With Whidbey, could use anonymous functions.
return new Substitution(new CreateSubstitutionClosure(map).Method);
}
private sealed class CreateSubstitutionClosure {
- Hashtable/*Variable!->Expr!*//*!*/ map;
+ Dictionary<Variable /*!*/, Expr /*!*/>/*!*/ map;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(map != null);
}
- public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map)
+ public CreateSubstitutionClosure(Dictionary<Variable, Expr> map)
: base() {
Contract.Requires(map != null);
this.map = map;
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 57910775..b7626d99 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -328,7 +328,7 @@ namespace Microsoft.Boogie { Contract.Requires(newModifies != null);
Contract.Requires(newLocalVars != null);
- Hashtable substMap = new Hashtable();
+ Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
Procedure proc = impl.Proc;
foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {
@@ -365,7 +365,7 @@ namespace Microsoft.Boogie { }
}
- Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();
+ Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();
foreach (IdentifierExpr/*!*/ mie in proc.Modifies) {
Contract.Assert(mie != null);
@@ -588,12 +588,12 @@ namespace Microsoft.Boogie { public Substitution Subst;
public Substitution OldSubst;
- public CodeCopier(Hashtable substMap) {
+ public CodeCopier(Dictionary<Variable, Expr> substMap) {
Contract.Requires(substMap != null);
Subst = Substituter.SubstitutionFromHashtable(substMap);
}
- public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) {
+ public CodeCopier(Dictionary<Variable, Expr> substMap, Dictionary<Variable, Expr> oldSubstMap) {
Contract.Requires(oldSubstMap != null);
Contract.Requires(substMap != null);
Subst = Substituter.SubstitutionFromHashtable(substMap);
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index b3b02724..6874f1c9 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -95,7 +95,7 @@ namespace Microsoft.Boogie { Set freeVars = new Set();
lambda.ComputeFreeVariables(freeVars);
// this is ugly, the output will depend on hashing order
- Hashtable subst = new Hashtable();
+ Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
VariableSeq formals = new VariableSeq();
ExprSeq callArgs = new ExprSeq();
ExprSeq axCallArgs = new ExprSeq();
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index e353700f..63f9557f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -281,7 +281,7 @@ namespace Microsoft.Boogie int count = 0;
while (callCmd != null)
{
- Hashtable map = new Hashtable();
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
foreach (Variable x in callCmd.Proc.InParams)
{
Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true);
@@ -317,7 +317,7 @@ namespace Microsoft.Boogie return proc;
}
- private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Hashtable map)
+ private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Dictionary<Variable, Expr> map)
{
if (yields.Count == 0) return;
@@ -354,8 +354,8 @@ namespace Microsoft.Boogie locals.Add(copy);
map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);
}
- Hashtable ogOldLocalMap = new Hashtable();
- Hashtable assumeMap = new Hashtable(map);
+ Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);
foreach (IdentifierExpr ie in globalMods)
{
Variable g = ie.Decl;
@@ -422,7 +422,7 @@ namespace Microsoft.Boogie Program program = linearTypechecker.program;
ProcedureInfo info = procNameToInfo[impl.Name];
- Hashtable map = new Hashtable();
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
foreach (Variable local in impl.LocVars)
{
var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));
@@ -717,7 +717,7 @@ namespace Microsoft.Boogie yields.Add(cmds);
cmds = new CmdSeq();
}
- CreateYieldCheckerImpl(proc, yields, new Hashtable());
+ CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());
}
private void AddYieldProcAndImpl()
|