From 768ee8abb31d912cfdc8eeaf41d7f44f1691ce0c Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Thu, 10 Mar 2011 17:37:58 +0000
Subject: 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.

---
 Source/VCExpr/Boogie2VCExpr.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/VCExpr/Boogie2VCExpr.cs')

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 64239e42..4d8fed6a 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.VCExprAST {
       private readonly List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ Mapping;
       [ContractInvariantMethod]
       void ObjectInvariant() {
-        Contract.Invariant(Mapping != null && Contract.ForAll(Mapping, i => cce.NonNullElements(i)));
+        Contract.Invariant(Mapping != null && Contract.ForAll(Mapping, i => cce.NonNullDictionaryAndValues(i)));
       }
 
 
@@ -147,7 +147,7 @@ namespace Microsoft.Boogie.VCExprAST {
         List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ mapping =
           new List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>();
         foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in vm.Mapping) {
-          Contract.Assert(cce.NonNullElements(d));
+          Contract.Assert(cce.NonNullDictionaryAndValues(d));
           mapping.Add(new Dictionary<VarKind/*!*/, VCExprVar/*!*/>(d));
         }
         this.Mapping = mapping;
-- 
cgit v1.2.3