diff options
| author |  mikebarnett <unknown> | 2011-03-10 17:37:58 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2011-03-10 17:37:58 +0000 |
| commit | 768ee8abb31d912cfdc8eeaf41d7f44f1691ce0c (patch) | |
| tree | 533ab6aa0d91c5a5e7c66125834fb5b8695ccf71 /Source/VCExpr/NameClashResolver.cs | |
| parent | e28c62b12194be07e3ecb3301e6b3e0336bcac2a (diff) | |
Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
Diffstat (limited to 'Source/VCExpr/NameClashResolver.cs')
| -rw-r--r-- | Source/VCExpr/NameClashResolver.cs | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs index 7c06af18..f811461d 100644 --- a/Source/VCExpr/NameClashResolver.cs +++ b/Source/VCExpr/NameClashResolver.cs @@ -58,12 +58,12 @@ namespace Microsoft.Boogie.VCExprAST { private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;
[ContractInvariantMethod]
void GlobalNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(GlobalNames));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalNames));
}
private readonly List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ LocalNames;
[ContractInvariantMethod]
void LocalNamesInvariantMethod() {
- Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullElements(i)));
+ Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullDictionaryAndValues(i)));
}
// dictionary of all names that have already been used
@@ -71,17 +71,17 @@ namespace Microsoft.Boogie.VCExprAST { private readonly IDictionary<string/*!*/, bool/*!*/>/*!*/ UsedNames;
[ContractInvariantMethod]
void UsedNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(UsedNames));
+ Contract.Invariant(UsedNames != null);
}
private readonly IDictionary<string/*!*/, int/*!*/>/*!*/ CurrentCounters;
[ContractInvariantMethod]
void CurrentCountersInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(CurrentCounters));
+ Contract.Invariant(CurrentCounters != null);
}
private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalPlusLocalNames;
[ContractInvariantMethod]
void GlobalPlusLocalNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(GlobalPlusLocalNames));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalPlusLocalNames));
}
////////////////////////////////////////////////////////////////////////////
|