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.

6 files changed, 43 insertions, 43 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 0a8a0de5..eb25a984 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1904,7 +1904,7 @@ namespace Microsoft.Boogie {
     }

 

     private IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ TypeParamSubstitution() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));

+      Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

       Contract.Assume(TypeParameters != null);

       IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

       foreach (TypeVariable/*!*/ v in TypeParameters.FormalTypeParams) {

@@ -2244,7 +2244,7 @@ namespace Microsoft.Boogie {
           Type.MatchArgumentTypes(Proc.TypeParameters,

                                   formalTypes, actualArgs, null, null,

                                   "call forall to " + callee, tc);

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

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

 

         InstantiatedTypes = new TypeSeq();

         foreach (Variable/*!*/ var in Proc.InParams) {

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 96bf358e..84703a7c 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -114,7 +114,7 @@ namespace Microsoft.Boogie {
 

     [Pure]

     public static bool IsIdempotent(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {

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

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

       return Contract.ForAll(unifier.Values, t => Contract.ForAll(0, t.FreeVariables.Length, var =>

                                    !unifier.ContainsKey(t.FreeVariables[var])));

     }

@@ -446,7 +446,7 @@ namespace Microsoft.Boogie {
       Contract.Requires((formalOuts == null) == (actualOuts == null));

       Contract.Requires(formalOuts == null || formalOuts.Length == cce.NonNull(actualOuts).Length);

       Contract.Requires(tc == null || opName != null);//Redundant

-      Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));

+      Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

 

       // requires "actualArgs" and "actualOuts" to have been type checked

 

@@ -538,7 +538,7 @@ namespace Microsoft.Boogie {
       IDictionary<TypeVariable/*!*/, Type/*!*/> subst =

         MatchArgumentTypes(typeParams, formalIns, actualIns,

                            actualOuts != null ? formalOuts : null, actualOuts, opName, tc);

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

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

       foreach (TypeVariable/*!*/ var in typeParams) {

         Contract.Assert(var != null);

         actualTypeParams.Add(subst[var]);

@@ -583,7 +583,7 @@ namespace Microsoft.Boogie {
 

       IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =

         InferTypeParameters(typeParams, formalArgs, actualArgs);

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

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

 

       Type/*!*/ res = formalResult.Substitute(subst);

       Contract.Assert(res != null);

@@ -634,7 +634,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(typeParams != null);

       Contract.Requires(formalArgs != null);

       Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Length == actualArgs.Length);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));

+      Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));

 

       

       TypeSeq proxies = new TypeSeq();

@@ -773,7 +773,7 @@ namespace Microsoft.Boogie {
       }

     }

     public override Type Clone(IDictionary<TypeVariable, TypeVariable> varMap) {

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

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

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

 

       throw new NotImplementedException();

@@ -796,13 +796,13 @@ namespace Microsoft.Boogie {
     public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary<TypeVariable, Type> unifier) {

       Contract.Requires(that != null);

       Contract.Requires(unifiableVariables != null);

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

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

       Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Has(key)));

       Contract.Requires(IsIdempotent(unifier));

       throw new NotImplementedException();

     }

     public override Type Substitute(IDictionary<TypeVariable, Type> subst) {

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

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

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

 

       throw new NotImplementedException();

@@ -1501,7 +1501,7 @@ Contract.Requires(that != null);
     private bool addSubstitution(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ oldSolution,

       // the type that "this" is instantiated with

                                  Type/*!*/ newSubst) {

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

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

       Contract.Requires(newSubst != null);

       Contract.Requires(!oldSolution.ContainsKey(this));

 

@@ -2276,7 +2276,7 @@ Contract.Requires(that != null);
       }

 

       public Constraint Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) {

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

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

         TypeSeq/*!*/ args = new TypeSeq();

         foreach (Type/*!*/ t in Arguments) {

           Contract.Assert(t != null);

@@ -2291,7 +2291,7 @@ Contract.Requires(that != null);
                         TypeVariableSeq/*!*/ unifiableVariables,

                         IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ result) {

         Contract.Requires(unifiableVariables != null);

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

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

         Contract.Requires(that != null);

         Contract.Requires(Arguments.Length == that.Arguments.Length);

         Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

@@ -3296,7 +3296,7 @@ Contract.Assert(var != null);
 

     [Pure]

     private bool collisionsPossible(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {

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

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

       // PR: could be written more efficiently

       return Contract.Exists(0, TypeParameters.Length, i => subst.ContainsKey(TypeParameters[i]) || Contract.Exists(subst.Values, t => t.FreeVariables.Has(TypeParameters[i])));

     }

@@ -3552,13 +3552,13 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
     private readonly IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ Instantiations;

     [ContractInvariantMethod]

     void InstantiationsInvariantMethod() {

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

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

     }

 

     public SimpleTypeParamInstantiation(List<TypeVariable/*!*/>/*!*/ typeParams,

                                         IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ instantiations) {

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

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

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

       this.TypeParams = typeParams;

       this.Instantiations = instantiations;

     }

@@ -3619,7 +3619,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
     void ObjectInvariant() {

       Contract.Invariant(Proxy != null);

       Contract.Invariant(ArgumentsResult != null);

-      Contract.Invariant(Instantiations == null || cce.NonNullElements(Instantiations));

+      Contract.Invariant(Instantiations == null || cce.NonNullDictionaryAndValues(Instantiations));

     }

 

 

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 22a8f160..c1270eab 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -44,7 +44,7 @@ namespace Microsoft.Boogie {
     static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

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

       Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v)));

     }

 

@@ -663,17 +663,17 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(graph.TopologicalSort()));

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

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

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

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

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

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

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

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

+      Contract.Invariant(priority != null);

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

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

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

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

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

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

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

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

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

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

       Contract.Invariant(summary != null);

       Contract.Invariant(impl != null);

     }

@@ -830,18 +830,18 @@ namespace Microsoft.Boogie {
       Contract.Invariant(workList != null);

       Contract.Invariant(mainImpl != null);

       Contract.Invariant(program != null);

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

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

-      Contract.Invariant(cce.NonNullElements(callers) &&

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

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(callers) &&

         Contract.ForAll(callers.Values, v => cce.NonNullElements(v)));

       Contract.Invariant(cce.NonNullElements(callGraph.TopologicalSort()));

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

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

-      Contract.Invariant(cce.NonNullElements(varsLiveAtExit) &&

+      Contract.Invariant(procPriority != null);

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

+      Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) &&

         Contract.ForAll(varsLiveAtExit.Values, v => cce.NonNullElements(v)));

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

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

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

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

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

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

     }

 

 

@@ -1081,7 +1081,7 @@ namespace Microsoft.Boogie {
       void ObjectInvariant() {

         Contract.Invariant(priorities != null);

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

-        Contract.Invariant(cce.NonNullElements(workList) &&

+        Contract.Invariant(cce.NonNullDictionaryAndValues(workList) &&

           Contract.ForAll(workList.Values, v => cce.NonNullElements(v)));

       }

 

diff --git a/Source/Core/GraphAlgorithms.cs b/Source/Core/GraphAlgorithms.cs
index 0815e54a..a19cf96c 100644
--- a/Source/Core/GraphAlgorithms.cs
+++ b/Source/Core/GraphAlgorithms.cs
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> {

+  public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> where Node : class {

     private readonly IDictionary<Node/*!*/, object>/*!*/ graph;

     [ContractInvariantMethod]

     void graphInvariantMethod() {

@@ -175,7 +175,7 @@ namespace Microsoft.Boogie {
     private readonly Stack<Node/*!*/>/*!*/ postOrder = new Stack<Node/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(seen != null && cce.NonNullElements(seen.Keys));

+      Contract.Invariant(seen != null);

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

     }

 

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 12f58b0a..6da85388 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -29,8 +29,8 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(codeCopier != null);

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

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

+      Contract.Invariant(recursiveProcUnrollMap != null);

+      Contract.Invariant(inlinedProcLblMap != null);

     }

 

 

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index 6976e281..91d8842a 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -108,7 +108,7 @@ namespace Microsoft.Boogie {
       public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block/*!*/, GraphNode/*!*/>/*!*/ gd, HashSet<Block> beingVisited) {

         Contract.Requires(beingVisited != null);

         Contract.Requires(b != null);

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

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

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

         GraphNode g;

         if (gd.TryGetValue(b, out g)) {

@@ -173,7 +173,7 @@ namespace Microsoft.Boogie {
     private LoopUnroll(int unrollMaxDepth, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal)

       : base() {//BASEMOVE DANGER

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

-      Contract.Requires(cce.NonNullElements(scc) && Contract.ForAll(scc.Values, v => cce.NonNullElements(v)));

+      Contract.Requires(cce.NonNullDictionaryAndValues(scc) && Contract.ForAll(scc.Values, v => cce.NonNullElements(v)));

       Contract.Requires(0 <= unrollMaxDepth);

       this.newBlockSeqGlobal = newBlockSeqGlobal;

       this.c = unrollMaxDepth;

@@ -187,7 +187,7 @@ namespace Microsoft.Boogie {
 

     private LoopUnroll(int unrollMaxDepth, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>> scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal, LoopUnroll head) {

       Contract.Requires(head != null);

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

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

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

       Contract.Requires(0 <= unrollMaxDepth);

       this.newBlockSeqGlobal = newBlockSeqGlobal;