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.

1 files changed, 2 insertions, 2 deletions

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;