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/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 49440ff0..552df3ed 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie {
     internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;

     [ContractInvariantMethod]

     void MiscInvariant() {

-      Contract.Invariant(cce.NonNullElements(SingletonOpDict));

+      Contract.Invariant(SingletonOpDict != null);

     }

 

 

@@ -693,7 +693,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return res;

     }

 

-    public static List<T/*!*/>/*!*/ ToNonNullList<T>(params T[] args) {

+    public static List<T/*!*/>/*!*/ ToNonNullList<T>(params T[] args) where T : class {

       Contract.Requires(args != null);

       List<T/*!*/>/*!*/ res = new List<T>(args.Length);

       foreach (T t in args)