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.

5 files changed, 23 insertions, 23 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));

     }

 

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 59a1331d..82cb6651 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -58,10 +58,10 @@ namespace Microsoft.Dafny {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(builtIns != null);

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(classes));

       Contract.Invariant(cce.NonNullElements(importGraph));

-      Contract.Invariant(cce.NonNullElements(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullElements(v)));

-      Contract.Invariant(cce.NonNullElements(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullElements(v)));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullDictionaryAndValues(v)));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));

     }

 

     bool checkRefinements = true; // used to indicate a cycle in refinements

@@ -1632,7 +1632,7 @@ namespace Microsoft.Dafny {
 

     public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/,Type/*!*/>/*!*/ subst) {

       Contract.Requires(type != null);

-      Contract.Requires(cce.NonNullElements(subst));

+      Contract.Requires(cce.NonNullDictionaryAndValues(subst));

       Contract.Ensures(Contract.Result<Type>() != null);

 

       if (type is BasicType) {

diff --git a/Dafny/SccGraph.cs b/Dafny/SccGraph.cs
index a3337ccc..9f4b22c5 100644
--- a/Dafny/SccGraph.cs
+++ b/Dafny/SccGraph.cs
@@ -4,7 +4,7 @@ using System.Diagnostics.Contracts;
 

 namespace Microsoft.Dafny {

 

-  public class Graph<Node>

+  public class Graph<Node> where Node : class

   {

     enum VisitedStatus { Unvisited, OnStack, Visited }

     class Vertex {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 6c1deb12..b641b69d 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -30,9 +30,9 @@ namespace Microsoft.Dafny {
     [ContractInvariantMethod]

     void ObjectInvariant() 

     {

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

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

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(classes));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(fields));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(fieldFunctions));

     }

 

     readonly Bpl.Program sink;

@@ -1030,7 +1030,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(calleeFrame));

       Contract.Requires(receiverReplacement != null);

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Requires(etran != null);

       Contract.Requires(builder != null);

       Contract.Requires(errorMessage != null);

@@ -1160,7 +1160,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(f != null);

       Contract.Requires(etran != null);

       Contract.Requires(cce.NonNullElements(rw));

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Requires(predef != null);

       Contract.Requires((receiverReplacement == null) == (substMap == null));

       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

@@ -2463,13 +2463,13 @@ namespace Microsoft.Dafny {
     {

       private readonly Dictionary<string,Bpl.Expr> subst;

       public NominalSubstituter(Dictionary<string,Bpl.Expr> subst) :base(){

-        Contract.Requires(cce.NonNullElements(subst));

+        Contract.Requires(cce.NonNullDictionaryAndValues(subst));

         this.subst = subst;

       }

 

       [ContractInvariantMethod]

       void ObjectInvariant() {

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

+        Contract.Invariant(cce.NonNullDictionaryAndValues(subst));

       }

 

           

@@ -3346,7 +3346,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(contextDecreases));

       Contract.Requires(cce.NonNullElements(calleeDecreases));

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Requires(etran != null);

       Contract.Requires(builder != null);

 

@@ -5249,7 +5249,7 @@ namespace Microsoft.Dafny {
 

     static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(Contract.Result<Expression>() != null);

 

       Expression newExpr = null;  // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end

@@ -5397,7 +5397,7 @@ namespace Microsoft.Dafny {
     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(cce.NonNullElements(elist));

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

       List<Expression> newElist = null;  // initialized lazily

       for (int i = 0; i < elist.Count; i++)

@@ -5422,7 +5422,7 @@ namespace Microsoft.Dafny {
     }

     

     static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       if (trigs != null) {

         List<Expression> terms = SubstituteExprList(trigs.Terms, receiverReplacement, substMap);

         Triggers prev = SubstTriggers(trigs.Prev, receiverReplacement, substMap);

@@ -5434,7 +5434,7 @@ namespace Microsoft.Dafny {
     }

 

     static Attributes SubstAttributes(Attributes attrs, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

-      Contract.Requires(cce.NonNullElements(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       if (attrs != null) {

         List<Attributes.Argument> newArgs = new List<Attributes.Argument>();  // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes

         bool anyArgSubst = false;

diff --git a/Dafny/cce.cs b/Dafny/cce.cs
index 8391361b..ff5152d0 100644
--- a/Dafny/cce.cs
+++ b/Dafny/cce.cs
@@ -10,24 +10,24 @@ using Microsoft.Boogie;
 

 public static class cce {

   [Pure]

-  public static T NonNull<T>(T t) {

+  public static T NonNull<T>(T t) where T : class {

     Contract.Assert(t != null);

     return t;

   }

   [Pure]

-  public static bool NonNullElements<T>(IEnumerable<T> collection) {

+  public static bool NonNullElements<T>(IEnumerable<T> collection) where T : class {

     return collection != null && Contract.ForAll(collection, c => c != null);

   }

   [Pure]

-  public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

-    return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values);

+  public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TValue> collection) where TValue : class {

+    return collection != null && NonNullElements(collection.Values);

   }

   [Pure]

   public static bool NonNullElements(VariableSeq collection) {

     return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

   }

   [Pure]

-  public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

+  public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) where T : class {

     return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

   }

   [Pure]