diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-22 14:33:46 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-22 14:33:46 +0100 |
| commit | a9a9bde95e700ef77ea5fee4ed7dd5a2fe04a46a (patch) | |
| tree | 66d11e82076a416c4e3842adf8737877ea29a400 | |
| parent | 3802281edec18eb2fd3e75de27f3eb72d93d44b0 (diff) | |
| parent | 5664c5e30f16b74eae4cdcb0b9ba65d5b030c815 (diff) | |
merge
30 files changed, 229 insertions, 276 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 5e69b179..e7c1fb77 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>();
@@ -2359,9 +2359,9 @@ namespace Microsoft.Boogie { }
public class Procedure : DeclWithFormals {
- public RequiresSeq/*!*/ Requires;
+ public List<Requires>/*!*/ Requires;
public IdentifierExprSeq/*!*/ Modifies;
- public EnsuresSeq/*!*/ Ensures;
+ public List<Ensures>/*!*/ Ensures;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Requires != null);
@@ -2376,7 +2376,7 @@ namespace Microsoft.Boogie { public readonly ProcedureSummary/*!*/ Summary;
public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,
- RequiresSeq/*!*/ requires, IdentifierExprSeq/*!*/ modifies, EnsuresSeq/*!*/ ensures)
+ List<Requires>/*!*/ requires, IdentifierExprSeq/*!*/ modifies, List<Ensures>/*!*/ ensures)
: this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -2390,7 +2390,7 @@ namespace Microsoft.Boogie { }
public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,
- RequiresSeq/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, EnsuresSeq/*!*/ @ensures, QKeyValue kv
+ List<Requires>/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, List<Ensures>/*!*/ @ensures, QKeyValue kv
)
: base(tok, name, typeParams, inParams, outParams) {
Contract.Requires(tok != null);
@@ -2531,7 +2531,7 @@ namespace Microsoft.Boogie { VariableSeq inputs, VariableSeq outputs, IdentifierExprSeq globalMods)
: base(Token.NoToken, impl.Name + "_loop_" + header.ToString(),
new TypeVariableSeq(), inputs, outputs,
- new RequiresSeq(), globalMods, new EnsuresSeq())
+ new List<Requires>(), globalMods, new List<Ensures>())
{
enclosingImpl = impl;
}
@@ -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(" --> ");
@@ -3224,39 +3224,6 @@ namespace Microsoft.Boogie { }
}
- public sealed class RequiresSeq : PureCollections.Sequence {
- public RequiresSeq(params Requires[]/*!*/ args)
- : base(args) {
- Contract.Requires(args != null);
- }
- public new Requires/*!*/ this[int index] {
- get {
- Contract.Ensures(Contract.Result<Requires>() != null);
-
- return cce.NonNull((Requires/*!*/)base[index]);
- }
- set {
- base[index] = value;
- }
- }
- }
-
- public sealed class EnsuresSeq : PureCollections.Sequence {
- public EnsuresSeq(params Ensures[]/*!*/ args)
- : base(args) {
- Contract.Requires(args != null);
- }
- public new Ensures/*!*/ this[int index] {
- get {
- Contract.Ensures(Contract.Result<Ensures>() != null);
- return cce.NonNull((Ensures/*!*/)base[index]);
- }
- set {
- base[index] = value;
- }
- }
- }
-
public sealed class VariableSeq : List<Variable> {
public VariableSeq(params Variable[]/*!*/ args)
: base(args) {
@@ -3266,14 +3233,6 @@ namespace Microsoft.Boogie { : base(varSeq) {
Contract.Requires(varSeq != null);
}
- public new Variable this[int index] {
- get {
- return (Variable)base[index];
- }
- set {
- base[index] = value;
- }
- }
public void Emit(TokenTextWriter stream, bool emitAttributes) {
Contract.Requires(stream != null);
string sep = "";
@@ -3303,7 +3262,7 @@ namespace Microsoft.Boogie { }
}
- public sealed class TypeSeq : PureCollections.Sequence {
+ public sealed class TypeSeq : List<Type> {
public TypeSeq(params Type[]/*!*/ args)
: base(args) {
Contract.Requires(args != null);
@@ -3312,19 +3271,9 @@ namespace Microsoft.Boogie { : base(varSeq) {
Contract.Requires(varSeq != null);
}
- public new Type/*!*/ this[int index] {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- return cce.NonNull((Type/*!*/)base[index]);
- }
- set {
- base[index] = value;
- }
- }
public List<Type/*!*/>/*!*/ ToList() {
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
- List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Length);
+ List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Count);
foreach (Type/*!*/ t in this) {
Contract.Assert(t != null);
res.Add(t);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 3005aaa6..47f5505e 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)
@@ -2113,7 +2113,7 @@ namespace Microsoft.Boogie { Substitution s = Substituter.SubstitutionFromHashtable(substMapBound);
bool hasWildcard = (wildcardVars.Length != 0);
Expr preConjunction = null;
- for (int i = 0; i < this.Proc.Requires.Length; i++) {
+ for (int i = 0; i < this.Proc.Requires.Count; i++) {
Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
if (!req.Free && !IsFree) {
if (hasWildcard) {
@@ -2149,7 +2149,7 @@ namespace Microsoft.Boogie { #region assume Pre[ins := cins] with formal paramters
if (hasWildcard) {
s = Substituter.SubstitutionFromHashtable(substMap);
- for (int i = 0; i < this.Proc.Requires.Length; i++) {
+ for (int i = 0; i < this.Proc.Requires.Count; i++) {
Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
if (!req.Free) {
Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
@@ -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/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 14534929..24622d8b 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1817,7 +1817,7 @@ namespace Microsoft.Boogie { tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
return null;
} else {
- Contract.Assert(actualResultType.Length == 1);
+ Contract.Assert(actualResultType.Count == 1);
tpInstantiation =
SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs);
return actualResultType[0];
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 8c355f72..81d44756 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -447,9 +447,9 @@ namespace Microsoft.Boogie { Contract.Requires(actualArgs != null);
Contract.Requires(opName != null);
Contract.Requires(tc != null);
- Contract.Requires(formalArgs.Length == actualArgs.Length);
+ Contract.Requires(formalArgs.Count == actualArgs.Length);
Contract.Requires((formalOuts == null) == (actualOuts == null));
- Contract.Requires(formalOuts == null || formalOuts.Length == cce.NonNull(actualOuts).Length);
+ Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Length);
Contract.Requires(tc == null || opName != null);//Redundant
Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));
@@ -462,7 +462,7 @@ namespace Microsoft.Boogie { subst.Add(tv, proxy);
}
- for (int i = 0; i < formalArgs.Length; i++) {
+ for (int i = 0; i < formalArgs.Count; i++) {
Type formal = formalArgs[i].Substitute(subst);
Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type);
// if the type variables to be matched occur in the actual
@@ -479,7 +479,7 @@ namespace Microsoft.Boogie { }
if (formalOuts != null) {
- for (int i = 0; i < formalOuts.Length; ++i) {
+ for (int i = 0; i < formalOuts.Count; ++i) {
Type formal = formalOuts[i].Substitute(subst);
Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type);
// if the type variables to be matched occur in the actual
@@ -524,13 +524,13 @@ namespace Microsoft.Boogie { Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));
actualTypeParams = new List<Type/*!*/>();
- if (formalIns.Length != actualIns.Length) {
+ if (formalIns.Count != actualIns.Length) {
tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",
opName, actualIns.Length);
// if there are no type parameters, we can still return the result
// type and hope that the type checking proceeds
return typeParams.Length == 0 ? formalOuts : null;
- } else if (actualOuts != null && formalOuts.Length != actualOuts.Length) {
+ } else if (actualOuts != null && formalOuts.Count != actualOuts.Length) {
tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",
opName, actualOuts.Length);
// if there are no type parameters, we can still return the result
@@ -638,7 +638,7 @@ namespace Microsoft.Boogie { TypeSeq/*!*/ actualArgs) {
Contract.Requires(typeParams != null);
Contract.Requires(formalArgs != null);
- Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Length == actualArgs.Length);
+ Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count);
Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));
@@ -651,7 +651,7 @@ namespace Microsoft.Boogie { subst.Add(tv, proxy);
}
- for (int i = 0; i < formalArgs.Length; i++) {
+ for (int i = 0; i < formalArgs.Count; i++) {
Type formal = formalArgs[i].Substitute(subst);
Type actual = actualArgs[i];
// if the type variables to be matched occur in the actual
@@ -1296,7 +1296,7 @@ Contract.Requires(that != null); }
}
if (is_bv) {
- if (Arguments.Length > 0) {
+ if (Arguments.Count > 0) {
rc.Error(this,
"bitvector types must not be applied to arguments: {0}",
Name);
@@ -1308,7 +1308,7 @@ Contract.Requires(that != null); // second case: the identifier is resolved to a type variable
TypeVariable var = rc.LookUpTypeBinder(Name);
if (var != null) {
- if (Arguments.Length > 0) {
+ if (Arguments.Count > 0) {
rc.Error(this,
"type variables must not be applied to arguments: {0}",
var);
@@ -1320,7 +1320,7 @@ Contract.Requires(that != null); // recursively resolve the arguments
TypeCtorDecl ctorDecl = rc.LookUpType(Name);
if (ctorDecl != null) {
- if (Arguments.Length != ctorDecl.Arity) {
+ if (Arguments.Count != ctorDecl.Arity) {
rc.Error(this,
"type constructor received wrong number of arguments: {0}",
ctorDecl);
@@ -1332,7 +1332,7 @@ Contract.Requires(that != null); // fourth case: the identifier denotes a type synonym
TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name);
if (synDecl != null) {
- if (Arguments.Length != synDecl.TypeParameters.Length) {
+ if (Arguments.Count != synDecl.TypeParameters.Length) {
rc.Error(this,
"type synonym received wrong number of arguments: {0}",
synDecl);
@@ -2304,7 +2304,7 @@ Contract.Requires(that != null); Contract.Requires(unifiableVariables != null);
Contract.Requires(cce.NonNullDictionaryAndValues(result));
Contract.Requires(that != null);
- Contract.Requires(Arguments.Length == that.Arguments.Length);
+ Contract.Requires(Arguments.Count == that.Arguments.Count);
Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
foreach (TypeVariable/*!*/ tv in that.TypeParameters) {
Contract.Assert(tv != null);
@@ -2313,7 +2313,7 @@ Contract.Requires(that != null); }
bool good = true;
- for (int i = 0; i < that.Arguments.Length; i++) {
+ for (int i = 0; i < that.Arguments.Count; i++) {
Type t0 = that.Arguments[i].Substitute(subst);
Type t1 = this.Arguments[i];
good &= t0.Unify(t1, unifiableVariables, result);
@@ -2332,7 +2332,7 @@ Contract.Requires(that != null); }
private void AddConstraint(Constraint c) {
- Contract.Requires(c.Arguments.Length == Arity);
+ Contract.Requires(c.Arguments.Count == Arity);
Type f = ProxyFor;
MapType mf = f as MapType;
@@ -2462,7 +2462,7 @@ Contract.Requires(that != null); return true;
} else if (that is MapType) {
MapType mapType = (MapType)that;
- if (mapType.Arguments.Length == Arity) {
+ if (mapType.Arguments.Count == Arity) {
bool good = true;
foreach (Constraint c in constraints)
good &= c.Unify(mapType, unifiableVariables, result);
@@ -2500,7 +2500,7 @@ Contract.Requires(that != null); // of the substituted variables (otherwise, we are in big trouble)
Contract.Assert(Contract.ForAll(constraints, c =>
Contract.ForAll(subst.Keys, var =>
- Contract.ForAll(0, c.Arguments.Length, t => !c.Arguments[t].FreeVariables.Has(var)) &&
+ Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Has(var)) &&
!c.Result.FreeVariables.Has(var))));
}
return base.Substitute(subst);
@@ -2566,7 +2566,7 @@ Contract.Requires(that != null); Contract.Requires(token != null);
Contract.Requires(decl != null);
Contract.Requires(arguments != null);
- Contract.Requires(arguments.Length == decl.TypeParameters.Length);
+ Contract.Requires(arguments.Count == decl.TypeParameters.Length);
this.Decl = decl;
this.Arguments = arguments;
@@ -2574,7 +2574,7 @@ Contract.Requires(that != null); // the type synonym
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
new Dictionary<TypeVariable/*!*/, Type/*!*/>();
- for (int i = 0; i < arguments.Length; ++i)
+ for (int i = 0; i < arguments.Count; ++i)
subst.Add(decl.TypeParameters[i], arguments[i]);
ExpandedType = decl.Body.Substitute(subst);
@@ -2830,7 +2830,7 @@ Contract.Requires(that != null); Contract.Requires(token != null);
Contract.Requires(decl != null);
Contract.Requires(arguments != null);
- Contract.Requires(arguments.Length == decl.Arity);
+ Contract.Requires(arguments.Count == decl.Arity);
this.Decl = decl;
this.Arguments = arguments;
}
@@ -2878,7 +2878,7 @@ Contract.Requires(that != null); CtorType thatCtorType = thatType as CtorType;
if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))
return false;
- if (Arguments.Length == 0)
+ if (Arguments.Count == 0)
return true;
return base.Equals(thatType);
}
@@ -2891,7 +2891,7 @@ Contract.Requires(that != null); CtorType thatCtorType = that as CtorType;
if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl))
return false;
- for (int i = 0; i < Arguments.Length; ++i) {
+ for (int i = 0; i < Arguments.Count; ++i) {
if (!Arguments[i].Equals(thatCtorType.Arguments[i],
thisBoundVariables, thatBoundVariables))
return false;
@@ -2913,7 +2913,7 @@ Contract.Requires(that != null); return false;
} else {
bool good = true;
- for (int i = 0; i < Arguments.Length; ++i)
+ for (int i = 0; i < Arguments.Count; ++i)
good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result);
return good;
}
@@ -2982,12 +2982,12 @@ Contract.Requires(that != null); Contract.Requires(stream != null);
Contract.Requires(args != null);
Contract.Requires(name != null);
- int opBindingStrength = args.Length > 0 ? 0 : 2;
+ int opBindingStrength = args.Count > 0 ? 0 : 2;
if (opBindingStrength < contextBindingStrength)
stream.Write("(");
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name));
- int i = args.Length;
+ int i = args.Count;
foreach (Type/*!*/ t in args) {
Contract.Assert(t != null);
stream.Write(" ");
@@ -3151,7 +3151,7 @@ Contract.Requires(that != null); MapType thatMapType = that as MapType;
if (thatMapType == null ||
this.TypeParameters.Length != thatMapType.TypeParameters.Length ||
- this.Arguments.Length != thatMapType.Arguments.Length)
+ this.Arguments.Count != thatMapType.Arguments.Count)
return false;
foreach (TypeVariable/*!*/ var in this.TypeParameters) {
@@ -3165,7 +3165,7 @@ Contract.Requires(that != null); try {
- for (int i = 0; i < Arguments.Length; ++i) {
+ for (int i = 0; i < Arguments.Count; ++i) {
if (!Arguments[i].Equals(thatMapType.Arguments[i],
thisBoundVariables, thatBoundVariables))
return false;
@@ -3197,7 +3197,7 @@ Contract.Requires(that != null); MapType thatMapType = that as MapType;
if (thatMapType == null ||
this.TypeParameters.Length != thatMapType.TypeParameters.Length ||
- this.Arguments.Length != thatMapType.Arguments.Length)
+ this.Arguments.Count != thatMapType.Arguments.Count)
return false;
// treat the bound variables of the two map types as equal...
@@ -3216,7 +3216,7 @@ Contract.Requires(that != null); }
// ... and then unify the domain and range types
bool good = true;
- for (int i = 0; i < this.Arguments.Length; i++) {
+ for (int i = 0; i < this.Arguments.Count; i++) {
Type t0 = this.Arguments[i].Substitute(subst0);
Type t1 = thatMapType.Arguments[i].Substitute(subst1);
good &= t0.Unify(t1, unifiableVariables, result);
@@ -3357,7 +3357,7 @@ Contract.Assert(var != null); [Pure]
public override int GetHashCode(TypeVariableSeq boundVariables) {
//Contract.Requires(boundVariables != null);
- int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Length;
+ int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Count;
foreach (TypeVariable/*!*/ var in this.TypeParameters) {
Contract.Assert(var != null);
@@ -3470,7 +3470,7 @@ Contract.Assert(var != null); }
public override int MapArity {
get {
- return Arguments.Length;
+ return Arguments.Count;
}
}
@@ -3498,7 +3498,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
return null;
} else {
- Contract.Assert(actualResult.Length == 1);
+ Contract.Assert(actualResult.Count == 1);
tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams);
return actualResult[0];
}
diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs index 30ca85ba..cac5068a 100644 --- a/Source/Core/BitvectorAnalysis.cs +++ b/Source/Core/BitvectorAnalysis.cs @@ -128,7 +128,7 @@ namespace Microsoft.Boogie { TypeSeq newArguments = new TypeSeq();
Type result = NewType(mapType.Result, mapDisjointSet.Result);
bool newTypeNeeded = (result != mapType.Result);
- for (int i = 0; i < mapType.Arguments.Length; i++) {
+ for (int i = 0; i < mapType.Arguments.Count; i++) {
if (mapDisjointSet.Args(i).Find() == uniqueBv32Set.Find()) {
newArguments.Add(new BvType(32));
newTypeNeeded = true;
@@ -151,7 +151,7 @@ namespace Microsoft.Boogie { if (mapType == null) {
return new DisjointSet();
}
- DisjointSet[] args = new DisjointSet[mapType.Arguments.Length];
+ DisjointSet[] args = new DisjointSet[mapType.Arguments.Count];
for (int i = 0; i < args.Length; i++) {
args[i] = MakeDisjointSet(mapType.Arguments[i]);
}
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 64ddbb50..9cd7d524 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -588,9 +588,9 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl> = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
TypeVariableSeq/*!*/ typeParams;
VariableSeq/*!*/ ins, outs;
- RequiresSeq/*!*/ pre = new RequiresSeq();
+ List<Requires>/*!*/ pre = new List<Requires>();
IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();
- EnsuresSeq/*!*/ post = new EnsuresSeq();
+ List<Ensures>/*!*/ post = new List<Ensures>();
VariableSeq/*!*/ locals = new VariableSeq();
StmtList/*!*/ stmtList;
@@ -642,7 +642,7 @@ ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVar .
-Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
+Spec<List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post>
= (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)
( "modifies"
[ Idents<out ms> (. foreach(IToken/*!*/ m in ms){
@@ -656,7 +656,7 @@ Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post> )
.
-SpecPrePost<bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post>
+SpecPrePost<bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post>
= (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .)
( "requires" (. tok = t; .)
{ Attribute<ref kv> }
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index fe189f83..1bea5880 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -353,27 +353,30 @@ 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;
}
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/Core/Inline.cs b/Source/Core/Inline.cs index 57910775..26d57f68 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);
@@ -453,7 +453,7 @@ namespace Microsoft.Boogie { }
// inject requires
- for (int i = 0; i < proc.Requires.Length; i++) {
+ for (int i = 0; i < proc.Requires.Count; i++) {
Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
inCmds.Add(InlinedRequires(callCmd, req));
}
@@ -529,7 +529,7 @@ namespace Microsoft.Boogie { CmdSeq outCmds = new CmdSeq();
// inject ensures
- for (int i = 0; i < proc.Ensures.Length; i++) {
+ for (int i = 0; i < proc.Ensures.Count; i++) {
Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
outCmds.Add(InlinedEnsures(callCmd, ens));
}
@@ -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/LinearSets.cs b/Source/Core/LinearSets.cs index 27312f38..1d541183 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -216,7 +216,7 @@ namespace Microsoft.Boogie MapType mapType = type as MapType;
if (mapType != null)
{
- if (mapType.Arguments.Length == 1 && mapType.Result.Equals(Type.Bool))
+ if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool))
{
type = mapType.Arguments[0];
if (type is MapType)
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index e353700f..bd6b1da3 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -176,7 +176,7 @@ namespace Microsoft.Boogie Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
inputs.Add(f);
}
- yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());
yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
}
@@ -275,13 +275,13 @@ namespace Microsoft.Boogie VariableSeq inParams = new VariableSeq();
VariableSeq outParams = new VariableSeq();
- RequiresSeq requiresSeq = new RequiresSeq();
- EnsuresSeq ensuresSeq = new EnsuresSeq();
+ List<Requires> requiresSeq = new List<Requires>();
+ List<Ensures> ensuresSeq = new List<Ensures>();
IdentifierExprSeq ieSeq = new IdentifierExprSeq();
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;
@@ -406,7 +406,7 @@ namespace Microsoft.Boogie // Create the yield checker procedure
var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);
- var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());
yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
yieldCheckerProcs.Add(yieldCheckerProc);
@@ -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));
@@ -504,7 +504,7 @@ namespace Microsoft.Boogie {
if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
{
- asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());
+ asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new List<Ensures>());
}
var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
@@ -639,7 +639,7 @@ namespace Microsoft.Boogie // Collect the yield predicates and desugar yields
List<CmdSeq> yields = new List<CmdSeq>();
CmdSeq cmds = new CmdSeq();
- if (proc.Requires.Length > 0)
+ if (proc.Requires.Count > 0)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
foreach (var domainName in linearTypechecker.linearDomains.Keys)
@@ -678,7 +678,7 @@ namespace Microsoft.Boogie yields.Add(cmds);
cmds = new CmdSeq();
}
- if (info.inParallelCall && proc.Ensures.Length > 0)
+ if (info.inParallelCall && proc.Ensures.Count > 0)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
foreach (var domainName in linearTypechecker.linearDomains.Keys)
@@ -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()
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 95c46934..7bd21d02 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -403,7 +403,7 @@ private class BvBounds : Expr { }
Bpl.Type ty = curr.Type;
var uti = ty as UnresolvedTypeIdentifier;
- if (uti != null && uti.Arguments.Length == 0) {
+ if (uti != null && uti.Arguments.Count == 0) {
// the given "thing" was just an identifier, so let's use it as the name of the parameter
curr.Name = uti.Name;
curr.Type = prevType;
@@ -470,9 +470,9 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
TypeVariableSeq/*!*/ typeParams;
VariableSeq/*!*/ ins, outs;
- RequiresSeq/*!*/ pre = new RequiresSeq();
+ List<Requires>/*!*/ pre = new List<Requires>();
IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();
- EnsuresSeq/*!*/ post = new EnsuresSeq();
+ List<Ensures>/*!*/ post = new List<Ensures>();
VariableSeq/*!*/ locals = new VariableSeq();
StmtList/*!*/ stmtList;
@@ -798,7 +798,7 @@ private class BvBounds : Expr { if (la.kind == 11) {
Get();
var uti = ty as UnresolvedTypeIdentifier;
- if (uti != null && uti.Arguments.Length == 0) {
+ if (uti != null && uti.Arguments.Count == 0) {
varName = uti.Name;
} else {
this.SemErr("expected identifier before ':'");
@@ -867,7 +867,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
}
- void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) {
+ void Spec(List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms;
if (la.kind == 34) {
Get();
@@ -897,7 +897,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StmtList(out stmtList);
}
- void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) {
+ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
if (la.kind == 36) {
Get();
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index ee873bd4..927b73fe 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -194,7 +194,7 @@ namespace Microsoft.Boogie { public virtual CtorType VisitCtorType(CtorType node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<CtorType>() != null);
- for (int i = 0; i < node.Arguments.Length; ++i)
+ for (int i = 0; i < node.Arguments.Count; ++i)
node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));
return node;
}
@@ -248,10 +248,10 @@ namespace Microsoft.Boogie { @requires.Condition = this.VisitExpr(@requires.Condition);
return @requires;
}
- public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
+ public virtual List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {
Contract.Requires(requiresSeq != null);
- Contract.Ensures(Contract.Result<RequiresSeq>() != null);
- for (int i = 0, n = requiresSeq.Length; i < n; i++)
+ Contract.Ensures(Contract.Result<List<Requires>>() != null);
+ for (int i = 0, n = requiresSeq.Count; i < n; i++)
requiresSeq[i] = this.VisitRequires(requiresSeq[i]);
return requiresSeq;
}
@@ -261,10 +261,10 @@ namespace Microsoft.Boogie { @ensures.Condition = this.VisitExpr(@ensures.Condition);
return @ensures;
}
- public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
+ public virtual List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {
Contract.Requires(ensuresSeq != null);
- Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
- for (int i = 0, n = ensuresSeq.Length; i < n; i++)
+ Contract.Ensures(Contract.Result<List<Ensures>>() != null);
+ for (int i = 0, n = ensuresSeq.Count; i < n; i++)
ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);
return ensuresSeq;
}
@@ -362,7 +362,7 @@ namespace Microsoft.Boogie { //
// NOTE: when overriding this method, you have to make sure that
// the bound variables of the map type are updated correctly
- for (int i = 0; i < node.Arguments.Length; ++i)
+ for (int i = 0; i < node.Arguments.Count; ++i)
node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));
node.Result = cce.NonNull((Type/*!*/)this.Visit(node.Result));
return node;
@@ -512,7 +512,7 @@ namespace Microsoft.Boogie { Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Type>() != null);
node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType));
- for (int i = 0; i < node.Arguments.Length; ++i)
+ for (int i = 0; i < node.Arguments.Count; ++i)
node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));
return node;
}
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index b317dc71..6b9f91cf 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -151,7 +151,7 @@ void ObjectInvariant() }
#region Attributes
- public Hashtable Label2Absy;
+ public Dictionary<int, Absy> Label2Absy;
public DoomErrorHandler ErrorHandler {
set {
m_ErrHandler = value;
@@ -219,9 +219,9 @@ void ObjectInvariant() }
- Label2Absy = new Hashtable(); // This is only a dummy
+ Label2Absy = new Dictionary<int, Absy>(); // This is only a dummy
m_Evc = new Evc(check);
- Hashtable l2a = null;
+ Dictionary<int, Absy> l2a = null;
VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
Contract.Assert(vce != null);
Contract.Assert( l2a!=null);
@@ -235,9 +235,9 @@ void ObjectInvariant() {
Contract.Requires(check != null);
m_Check = check;
- Label2Absy = new Hashtable(); // This is only a dummy
+ Label2Absy = new Dictionary<int, Absy>(); // This is only a dummy
m_Evc = new Evc(check);
- Hashtable l2a = null;
+ Dictionary<int, Absy> l2a = null;
int assertionCount; // compute and then ignore
VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
Contract.Assert(vce != null);
@@ -301,14 +301,14 @@ void ObjectInvariant() */
- VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) {
+ VCExpr GenerateEVC(Implementation impl, out Dictionary<int, Absy> label2absy, Checker ch, out int assertionCount) {
Contract.Requires(impl != null);
Contract.Requires(ch != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
TypecheckingContext tc = new TypecheckingContext(null);
impl.Typecheck(tc);
- label2absy = new Hashtable/*<int, Absy!>*/();
+ label2absy = new Dictionary<int, Absy>();
VCExpr vc;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Doomed:
@@ -322,7 +322,7 @@ void ObjectInvariant() }
public VCExpr LetVC(Block startBlock,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount)
{
@@ -342,7 +342,7 @@ void ObjectInvariant() }
VCExpr LetVC(Block block,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
Hashtable/*<Block, VCExprVar!>*/ blockVariables,
List<VCExprLetBinding> bindings,
ProverContext proverCtxt,
diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs index 33d8b68e..a85adbe1 100644 --- a/Source/Doomed/DoomErrorHandler.cs +++ b/Source/Doomed/DoomErrorHandler.cs @@ -15,7 +15,7 @@ namespace VC internal class DoomErrorHandler : ProverInterface.ErrorHandler
{
- protected Hashtable label2Absy;
+ protected Dictionary<int, Absy> label2Absy;
protected VerifierCallback callback;
private List<Block> m_CurrentTrace = new List<Block>();
@@ -28,7 +28,7 @@ namespace VC }
- public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback)
+ public DoomErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback)
{
Contract.Requires(label2Absy != null);
Contract.Requires(callback != null);
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 778ae767..341644ca 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -584,7 +584,7 @@ namespace VC { #region Program Passification
private void GenerateHelperBlocks(Implementation impl) {
Contract.Requires(impl != null);
- Hashtable gotoCmdOrigins = new Hashtable();
+ Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
Contract.Assert(exitBlock != null);
@@ -622,7 +622,7 @@ namespace VC { }
- private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {
+ private Dictionary<Variable, Expr> PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {
Contract.Requires(impl != null);
Contract.Requires(mvInfo != null);
Contract.Requires(this.exitBlock != null);
@@ -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;
@@ -744,14 +744,14 @@ namespace VC { ResetPredecessors(impl.Blocks);
//EmitImpl(impl,false);
- Hashtable/*Variable->Expr*/ htbl = PassifyProgram(impl, new ModelViewInfo(program, impl));
+ Dictionary<Variable, Expr> var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl));
// Collect the last incarnation of each reachability variable in the passive program
foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)
{
- if (htbl.ContainsKey(kvp.Value))
+ if (var2Expr.ContainsKey(kvp.Value))
{
- m_LastReachVarIncarnation[kvp.Value] = (Expr)htbl[kvp.Value];
+ m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value];
}
}
}
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),
diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index 8419471e..83be688e 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -312,13 +312,13 @@ public class BlockPredicator { if (dwf is Procedure)
{
var proc = (Procedure)dwf;
- var newRequires = new RequiresSeq();
+ var newRequires = new List<Requires>();
foreach (Requires r in proc.Requires)
{
newRequires.Add(new Requires(r.Free,
new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
}
- var newEnsures = new EnsuresSeq();
+ var newEnsures = new List<Ensures>();
foreach (Ensures e in proc.Ensures)
{
newEnsures.Add(new Ensures(e.Free,
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index cac6d95b..37bcda96 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -704,9 +704,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false);
throw new cce.UnreachableException();
}
- public override RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
+ public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {
//Contract.Requires(requiresSeq != null);
- Contract.Ensures(Contract.Result<RequiresSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Requires>>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
@@ -716,9 +716,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false);
throw new cce.UnreachableException();
}
- public override EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
+ public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {
//Contract.Requires(ensuresSeq != null);
- Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Ensures>>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 9d366c9f..c4a54300 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -469,7 +469,7 @@ namespace Microsoft.Boogie.TypeErasure { //
CtorType ctype = type.AsCtor;
Function/*!*/ repr = GetTypeCtorRepr(ctype.Decl);
- List<VCExpr/*!*/>/*!*/ args = new List<VCExpr/*!*/>(ctype.Arguments.Length);
+ List<VCExpr/*!*/>/*!*/ args = new List<VCExpr/*!*/>(ctype.Arguments.Count);
foreach (Type/*!*/ t in ctype.Arguments) {
Contract.Assert(t != null);
args.Add(Type2Term(t, varMapping));
@@ -970,7 +970,7 @@ namespace Microsoft.Boogie.TypeErasure { MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);
MapTypeClassRepresentation repr = GetClassRepresentation(abstraction);
- Contract.Assume(repr.RepresentingType.Arity == instantiations.Length);
+ Contract.Assume(repr.RepresentingType.Arity == instantiations.Count);
return new CtorType(Token.NoToken, repr.RepresentingType, instantiations);
}
@@ -1004,7 +1004,7 @@ namespace Microsoft.Boogie.TypeErasure { // Bingo!
// if the type does not contain any bound variables, we can simply
// replace it with a type variable
- TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Length);
+ TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Count);
Contract.Assume(!boundTypeParams.Has(abstractionVar));
instantiations.Add(rawType);
return abstractionVar;
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index 57218a73..49c7fe8e 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -180,7 +180,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); int typeParamNum = abstractedType.FreeVariables.Length +
abstractedType.TypeParameters.Length;
- int arity = typeParamNum + abstractedType.Arguments.Length;
+ int arity = typeParamNum + abstractedType.Arguments.Count;
Type/*!*/[]/*!*/ selectTypes = new Type/*!*/ [arity + 2];
Type/*!*/[]/*!*/ storeTypes = new Type/*!*/ [arity + 3];
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index df14eb01..44eb7dbb 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -307,11 +307,11 @@ namespace Microsoft.Boogie.TypeErasure // nothing
} else if (completeType.IsCtor) {
CtorType/*!*/ ctorType = completeType.AsCtor;
- if (ctorType.Arguments.Length > 0) {
+ if (ctorType.Arguments.Count > 0) {
// otherwise there are no chances of extracting any
// instantiations from this type
TypeCtorRepr repr = GetTypeCtorReprStruct(ctorType.Decl);
- for (int i = 0; i < ctorType.Arguments.Length; ++i) {
+ for (int i = 0; i < ctorType.Arguments.Count; ++i) {
VCExpr/*!*/ newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
Contract.Assert(newInnerTerm != null);
TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors);
@@ -644,7 +644,7 @@ namespace Microsoft.Boogie.TypeErasure typeParams.AddRange(abstractedType.TypeParameters.ToList());
typeParams.AddRange(abstractedType.FreeVariables.ToList());
- originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Length + 1);
+ originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);
TypeSeq/*!*/ mapTypeParams = new TypeSeq();
foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {
Contract.Assert(var != null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 0d6e2aab..dbe20415 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -257,14 +257,15 @@ namespace Microsoft.Boogie { var s = states[i];
if (0 <= s && s < MvInfo.CapturePoints.Count) {
VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];
- var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable();
+ var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Dictionary<Variable, Expr>();
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;
@@ -578,7 +579,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;
@@ -756,7 +757,7 @@ namespace VC { /// already been constructed for the implementation (and so
/// is already an element of impl.Blocks)
/// </param>
- protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins) {
+ protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {
Contract.Requires(impl != null);
Contract.Requires(unifiedExitBlock != null);
Contract.Requires(gotoCmdOrigins != null);
@@ -1085,7 +1086,7 @@ namespace VC { }
- protected Block GenerateUnifiedExit(Implementation impl, Hashtable gotoCmdOrigins) {
+ protected Block GenerateUnifiedExit(Implementation impl, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins) {
Contract.Requires(impl != null);
Contract.Requires(gotoCmdOrigins != null);
Contract.Ensures(Contract.Result<Block>() != null);
@@ -1112,7 +1113,7 @@ namespace VC { BlockSeq bs = new BlockSeq();
bs.Add(unifiedExit);
GotoCmd go = new GotoCmd(Token.NoToken, labels, bs);
- gotoCmdOrigins[go] = b.TransferCmd;
+ gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd;
b.TransferCmd = go;
unifiedExit.Predecessors.Add(b);
}
@@ -1162,7 +1163,7 @@ namespace VC { int currentIncarnationNumber =
variable2SequenceNumber.ContainsKey(x)
?
- (int)cce.NonNull(variable2SequenceNumber[x])
+ variable2SequenceNumber[x]
:
-1;
Variable v = new Incarnation(x, currentIncarnationNumber + 1);
@@ -1187,31 +1188,31 @@ namespace VC { /// <param name="b"></param>
/// <param name="block2Incarnation">Gives incarnation maps for b's predecessors.</param>
/// <returns></returns>
- protected Hashtable /*Variable -> Expr*/ ComputeIncarnationMap(Block b, Hashtable /*Variable -> Expr*/ block2Incarnation) {
+ protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b, Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation) {
Contract.Requires(b != null);
Contract.Requires(block2Incarnation != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
if (b.Predecessors.Length == 0) {
- return new Hashtable();
+ return new Dictionary<Variable, Expr>();
}
- Hashtable /*Variable -> Expr*/ incarnationMap = null;
+ Dictionary<Variable, Expr> incarnationMap = null;
Set /*Variable*/ fixUps = new Set /*Variable*/ ();
foreach (Block pred in b.Predecessors) {
Contract.Assert(pred != null);
- Contract.Assert(block2Incarnation.Contains(pred)); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet
- Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)block2Incarnation[pred];
+ Contract.Assert(block2Incarnation.ContainsKey(pred)); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet
+ Dictionary<Variable, Expr> predMap = (Dictionary<Variable, Expr>)block2Incarnation[pred];
Contract.Assert(predMap != null);
if (incarnationMap == null) {
- incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone();
+ incarnationMap = new Dictionary<Variable, Expr>(predMap);
continue;
}
ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ ();
foreach (Variable v in incarnationMap.Keys) {
Contract.Assert(v != null);
- if (!predMap.Contains(v)) {
+ if (!predMap.ContainsKey(v)) {
// conflict!!
conflicts.Add(v);
fixUps.Add(v);
@@ -1224,7 +1225,7 @@ namespace VC { }
foreach (Variable v in predMap.Keys) {
Contract.Assert(v != null);
- if (!incarnationMap.Contains(v)) {
+ if (!incarnationMap.ContainsKey(v)) {
// v was not in the domain of the predecessors seen so far, so it needs to be fixed up
fixUps.Add(v);
} else {
@@ -1251,10 +1252,10 @@ namespace VC { Contract.Assert(pred != null);
#region Create an assume command equating v_prime with its last incarnation in pred
#region Create an identifier expression for the last incarnation in pred
- Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]);
+ 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);
@@ -1279,9 +1280,9 @@ namespace VC { return incarnationMap;
}
- Hashtable preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement
+ Dictionary<Variable, Expr> preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement
- protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {
+ protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {
Contract.Requires(b != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(mvInfo != null);
@@ -1304,11 +1305,11 @@ namespace VC { #endregion
}
- protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {
+ protected Dictionary<Variable, Expr> Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {
Contract.Requires(impl != null);
Contract.Requires(mvInfo != null);
- Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
+ Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
RestoreParamWhereClauses(impl);
@@ -1322,7 +1323,7 @@ namespace VC { return r;
}
- protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {
+ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {
Contract.Requires(blocks != null);
Contract.Requires(modifies != null);
Contract.Requires(mvInfo != null);
@@ -1349,13 +1350,13 @@ namespace VC { // Now we can process the nodes in an order so that we're guaranteed to have
// processed all of a node's predecessors before we process the node.
- Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();
+ Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation = new Dictionary<Block, Dictionary<Variable, Expr>>();
Block exitBlock = null;
- Hashtable exitIncarnationMap = null;
+ Dictionary<Variable, Expr> exitIncarnationMap = null;
foreach (Block b in sortedNodes) {
Contract.Assert(b != null);
- Contract.Assert(!block2Incarnation.Contains(b));
- Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
+ Contract.Assert(!block2Incarnation.ContainsKey(b));
+ Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
// b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.
b.liveVarsBefore = null;
@@ -1398,11 +1399,11 @@ namespace VC { /// </summary>
protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)
{
- Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
+ Dictionary<Variable, Expr> oldFrameMap = new Dictionary<Variable, Expr>();
foreach (IdentifierExpr ie in modifies)
{
Contract.Assert(ie != null);
- if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))
+ if (!oldFrameMap.ContainsKey(cce.NonNull(ie.Decl)))
oldFrameMap.Add(ie.Decl, ie);
}
return Substituter.SubstitutionFromHashtable(oldFrameMap);
@@ -1412,7 +1413,7 @@ namespace VC { /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc
/// Meanwhile, record any information needed to later reconstruct a model view.
/// </summary>
- protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {
+ protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {
Contract.Requires(c != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(oldFrameSubst != null);
@@ -1432,14 +1433,14 @@ namespace VC { if (description != null) {
Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));
copy = Bpl.Expr.And(mv, copy);
- mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone()));
+ mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap)));
}
}
Contract.Assert(copy != null);
if (pc is AssertCmd) {
((AssertCmd)pc).OrigExpr = pc.Expr;
Contract.Assert(((AssertCmd)pc).IncarnationMap == null);
- ((AssertCmd)pc).IncarnationMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(incarnationMap.Clone());
+ ((AssertCmd)pc).IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));
}
pc.Expr = copy;
passiveCmds.Add(pc);
@@ -1518,7 +1519,7 @@ namespace VC { #region havoc w |--> assume whereClauses, out := in( w |-> w' )
else if (c is HavocCmd) {
if (this.preHavocIncarnationMap == null) // Save a copy of the incarnation map (at the top of a sequence of havoc statements)
- this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();
+ this.preHavocIncarnationMap = new Dictionary<Variable, Expr>(incarnationMap);
HavocCmd hc = (HavocCmd)c;
Contract.Assert(c != null);
@@ -1748,8 +1749,8 @@ namespace VC { public class Mapping
{
public readonly string Description;
- public readonly Hashtable /*Variable -> Expr*/ IncarnationMap;
- public Mapping(string description, Hashtable /*Variable -> Expr*/ incarnationMap) {
+ public readonly Dictionary<Variable, Expr> IncarnationMap;
+ public Mapping(string description, Dictionary<Variable, Expr> incarnationMap) {
Description = description;
IncarnationMap = incarnationMap;
}
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 3299ef76..78ed8cb5 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);
@@ -395,7 +395,7 @@ namespace Microsoft.Boogie public Dictionary<Incarnation, Absy> incarnationOriginMap;
public Hashtable /*Variable->Expr*/ exitIncarnationMap;
public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins;
- public Hashtable/*<int, Absy!>*/ label2absy;
+ public Dictionary<int, Absy> label2absy;
public VC.ModelViewInfo mvInfo;
public Dictionary<Block, VCExprVar> reachVars;
@@ -514,7 +514,7 @@ namespace Microsoft.Boogie //public VCExpr vcexpr;
//public List<VCExprVar> interfaceExprVars;
//public List<VCExprVar> privateExprVars;
- //public Hashtable/*<int, Absy!>*/ label2absy;
+ //public Dictionary<int, Absy> label2absy;
//public VC.ModelViewInfo mvInfo;
//public Dictionary<Block, List<CallSite>> callSites;
//public Dictionary<Block, List<CallSite>> recordProcCallSites;
@@ -1007,7 +1007,7 @@ namespace Microsoft.Boogie ConvertCFG2DAG(impl,edgesCut);
VC.ModelViewInfo mvInfo;
PassifyImpl(impl, out mvInfo);
- Hashtable/*<int, Absy!>*/ label2absy = null;
+ Dictionary<int, Absy> label2absy = null;
VCExpressionGenerator gen = checker.VCExprGen;
Contract.Assert(gen != null);
VCExpr vcexpr;
@@ -1871,7 +1871,7 @@ namespace Microsoft.Boogie Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);
VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];
var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)
- ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();
+ ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();
var cs = m.MkState(map.Description);
foreach (Variable v in info.AllVariables)
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index f90788d7..da413984 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -185,7 +185,7 @@ namespace VC { public VCExpr vcexpr;
public List<VCExprVar> interfaceExprVars;
public List<VCExprVar> privateExprVars;
- public Hashtable/*<int, Absy!>*/ label2absy;
+ public Dictionary<int, Absy> label2absy;
public ModelViewInfo mvInfo;
public Dictionary<Block, List<CallSite>> callSites;
public Dictionary<Block, List<CallSite>> recordProcCallSites;
@@ -1151,7 +1151,7 @@ namespace VC { // Get the VC of the current procedure
VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;
- Hashtable/*<int, Absy!>*/ mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
+ Dictionary<int, Absy> mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
// Find all procedure calls in vc and put labels on them
FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
@@ -1349,7 +1349,7 @@ namespace VC { StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];
info.GenerateVC();
VCExpr vc = info.vcexpr;
- Hashtable mainLabel2absy = info.label2absy;
+ Dictionary<int, Absy> mainLabel2absy = info.label2absy;
var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info);
// Find all procedure calls in vc and put labels on them
@@ -1851,7 +1851,7 @@ namespace VC { // VCs with different labels each time)
public class FCallHandler : MutatingVCExprVisitor<bool> {
Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
- public readonly Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy;
+ public readonly Dictionary<int, Absy>/*!*/ mainLabel2absy;
public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;
public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
@@ -1910,7 +1910,7 @@ namespace VC { public FCallHandler(VCExpressionGenerator/*!*/ gen,
Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
- string mainProcName, Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy)
+ string mainProcName, Dictionary<int, Absy>/*!*/ mainLabel2absy)
: base(gen) {
Contract.Requires(gen != null);
Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
@@ -2116,7 +2116,7 @@ namespace VC { return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);
}
- public Hashtable/*<int,absy>*/ getLabel2absy() {
+ public Dictionary<int, Absy> getLabel2absy() {
Contract.Ensures(Contract.Result<Hashtable>() != null);
Contract.Assert(currProc != null);
@@ -2158,7 +2158,7 @@ namespace VC { string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
if (lop.label.Substring(1).StartsWith(prefix)) {
int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
- Hashtable label2absy = getLabel2absy();
+ Dictionary<int, Absy> label2absy = getLabel2absy();
Absy cmd = label2absy[id] as Absy;
//label2absy.Remove(id);
@@ -2472,7 +2472,7 @@ namespace VC { Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);
VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];
var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)
- ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();
+ ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary<Variable, Expr>();
var cs = m.MkState(map.Description);
foreach (Variable v in info.AllVariables) {
@@ -2718,7 +2718,7 @@ namespace VC { Contract.Ensures(Contract.Result<Absy>() != null);
int id = int.Parse(label);
- Hashtable l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
+ Dictionary<int, Absy> l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
return cce.NonNull((Absy)l2a[id]);
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 80ffa072..09874382 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -290,7 +290,7 @@ namespace VC { parent.CurrentLocalVariables = impl.LocVars;
ModelViewInfo mvInfo;
parent.PassifyImpl(impl, out mvInfo);
- Hashtable label2Absy;
+ Dictionary<int, Absy> label2Absy;
Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
@@ -441,7 +441,7 @@ namespace VC { }
class ErrorHandler : ProverInterface.ErrorHandler {
- Hashtable label2Absy;
+ Dictionary<int, Absy> label2Absy;
VerifierCallback callback;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -450,7 +450,7 @@ namespace VC { }
- public ErrorHandler(Hashtable label2Absy, VerifierCallback callback) {
+ public ErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback) {
Contract.Requires(label2Absy != null);
Contract.Requires(callback != null);
this.label2Absy = label2Absy;
@@ -531,7 +531,7 @@ namespace VC { double total_cost;
int assertion_count;
double assertion_cost; // without multiplication by paths
- Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;
+ Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;
readonly public VCGen/*!*/ parent;
Implementation/*!*/ impl;
@@ -548,7 +548,7 @@ namespace VC { private int splitNo;
internal ErrorReporter reporter;
- public Split(List<Block/*!*/>/*!*/ blocks, Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {
+ public Split(List<Block/*!*/>/*!*/ blocks, Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {
Contract.Requires(cce.NonNullElements(blocks));
Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(par != null);
@@ -974,14 +974,14 @@ namespace VC { copies.Clear();
CloneBlock(blocks[0]);
List<Block> newBlocks = new List<Block>();
- Hashtable newGotoCmdOrigins = new Hashtable();
+ Dictionary<TransferCmd, ReturnCmd> newGotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
foreach (Block b in blocks) {
Contract.Assert(b != null);
Block tmp;
if (copies.TryGetValue(b, out tmp)) {
newBlocks.Add(cce.NonNull(tmp));
- if (gotoCmdOrigins.ContainsKey(b)) {
- newGotoCmdOrigins[tmp] = gotoCmdOrigins[b];
+ if (gotoCmdOrigins.ContainsKey(b.TransferCmd)) {
+ newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd];
}
foreach (Block p in b.Predecessors) {
@@ -1219,7 +1219,7 @@ namespace VC { this.checker = checker;
- Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
+ Dictionary<int, Absy> label2absy = new Dictionary<int, Absy>();
ProverContext ctx = checker.TheoremProver.Context;
Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
@@ -1228,14 +1228,14 @@ 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
ResetPredecessors(codeExpr.Blocks);
vcgen.AddBlocksBetween(codeExpr.Blocks);
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));
+ Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));
int ac; // computed, but then ignored for this CodeExpr
VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
@@ -1350,18 +1350,18 @@ namespace VC { }
#endregion
- public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
{
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- label2absy = new Hashtable/*<int, Absy!>*/();
+ label2absy = new Dictionary<int, Absy>();
return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
}
- protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext) {
+ protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1653,8 +1653,8 @@ namespace VC { }
public class ErrorReporter : ProverInterface.ErrorHandler {
- Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;
- Hashtable/*<int, Absy!>*//*!*/ label2absy;
+ Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;
+ Dictionary<int, Absy>/*!*/ label2absy;
List<Block/*!*/>/*!*/ blocks;
protected Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap;
protected VerifierCallback/*!*/ callback;
@@ -1686,8 +1686,8 @@ namespace VC { protected ProverContext/*!*/ context;
Program/*!*/ program;
- public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
- Hashtable/*<int, Absy!>*//*!*/ label2absy,
+ public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
+ Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
VerifierCallback/*!*/ callback,
@@ -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;
@@ -1782,8 +1782,8 @@ namespace VC { }
public class ErrorReporterLocal : ErrorReporter {
- public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
- Hashtable/*<int, Absy!>*//*!*/ label2absy,
+ public ErrorReporterLocal(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
+ Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
VerifierCallback/*!*/ callback,
@@ -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
@@ -2097,13 +2097,13 @@ namespace VC { }
}
- public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
+ public Dictionary<TransferCmd, ReturnCmd> PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
{
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();
+ Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
#region Debug Tracing
@@ -2216,7 +2216,7 @@ namespace VC { cmds.AddRange(entryBlock.Cmds);
entryBlock.Cmds = cmds;
// Make sure that all added commands are passive commands.
- Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());
+ Dictionary<Variable, Expr> incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary<Block, Dictionary<Variable, Expr>>());
TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,
ComputeOldExpressionSubstitution(impl.Proc.Modifies));
}
@@ -2530,7 +2530,7 @@ namespace VC { static VCExpr LetVC(Block startBlock,
VCExpr controlFlowVariableExpr,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount) {
Contract.Requires(startBlock != null);
@@ -2546,7 +2546,7 @@ namespace VC { static VCExpr LetVCIterative(List<Block> blocks,
VCExpr controlFlowVariableExpr,
- Hashtable label2absy,
+ Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount) {
Contract.Requires(blocks != null);
@@ -2616,7 +2616,7 @@ namespace VC { static VCExpr LetVC(Block block,
VCExpr controlFlowVariableExpr,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
Hashtable/*<Block, VCExprVar!>*/ blockVariables,
List<VCExprLetBinding/*!*/>/*!*/ bindings,
ProverContext proverCtxt,
@@ -2683,7 +2683,7 @@ namespace VC { static VCExpr DagVC(Block block,
VCExpr controlFlowVariableExpr,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
Hashtable/*<Block, VCExpr!>*/ blockEquations,
ProverContext proverCtxt,
out int assertionCount)
@@ -2738,7 +2738,7 @@ namespace VC { }
static VCExpr FlatBlockVC(Implementation impl,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
bool local, bool reach, bool doomed,
ProverContext proverCtxt,
out int assertionCount)
@@ -2874,7 +2874,7 @@ namespace VC { }
static VCExpr NestedBlockVC(Implementation impl,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
bool reach,
ProverContext proverCtxt,
out int assertionCount){
@@ -2997,7 +2997,7 @@ namespace VC { }
static VCExpr VCViaStructuredProgram
- (Implementation impl, Hashtable/*<int, Absy!>*/ label2absy,
+ (Implementation impl, Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount)
{
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index d82310ee..eed4e2a5 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -20,19 +20,19 @@ namespace VC { Contract.Invariant(Ctxt != null);
}
- [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;
+ [Rep] public readonly Dictionary<int, Absy> Label2absy;
[Rep] public readonly ProverContext Ctxt;
public readonly VCExpr ControlFlowVariableExpr;
public int AssertionCount; // counts the number of assertions for which Wlp has been computed
- public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)
+ public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt)
{
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
}
- public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)
+ public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)
{
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
|