summaryrefslogtreecommitdiff
path: root/Dafny/DafnyAst.cs
diff options
context:
space:
mode:
authorGravatar mikebarnett <unknown>2011-03-10 17:37:58 +0000
committerGravatar mikebarnett <unknown>2011-03-10 17:37:58 +0000
commita42f800cad7918d42349914a4b8f0d58d95d6531 (patch)
treee3f84afafefa83a5add6fd34299e29801a832b6f /Dafny/DafnyAst.cs
parentb9f45ea020cab2f5ce7de69a60dc6a19f7df810e (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 'Dafny/DafnyAst.cs')
-rw-r--r--Dafny/DafnyAst.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index d2536aa4..a8acb013 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -247,7 +247,7 @@ namespace Microsoft.Dafny {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(tok != null);
- Contract.Invariant(cce.NonNullElements(Name));
+ Contract.Invariant(Name != null);
Contract.Invariant(cce.NonNullElements(TypeArgs));
}