diff options
34 files changed, 195 insertions, 192 deletions
diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs index 8d7f6c45..005c9b17 100644 --- a/Source/AIFramework/Lattice.cs +++ b/Source/AIFramework/Lattice.cs @@ -489,8 +489,8 @@ namespace Microsoft.AbstractInterpretationFramework { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Map != null);
- Contract.Invariant(cce.NonNullElements(emptyDictionary1) && Contract.ForAll(emptyDictionary1.Values, set =>/*cce.NonNullElements(set)*/set != null));
- Contract.Invariant(cce.NonNullElements(emptyDictionary2));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary1) && Contract.ForAll(emptyDictionary1.Values, set =>/*cce.NonNullElements(set)*/set != null));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary2));
Contract.Invariant(indexMap != null);
Contract.Invariant(reverseIndexMap != null);
diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs index 64b6527a..71462c07 100644 --- a/Source/CodeContractsExtender/cce.cs +++ b/Source/CodeContractsExtender/cce.cs @@ -15,18 +15,18 @@ public static class cce { // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
//}
[Pure]
- public static T NonNull<T>(T t) {
+ public static T NonNull<T>(T t) where T : class {
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<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 && Contract.ForAll(collection, pair => NonNullElements(pair));
+ public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TValue> collection) where TValue : class {
+ return collection != null && cce.NonNullElements(collection.Values);
}
//[Pure]
//public static bool NonNullElements(VariableSeq collection) {
@@ -40,7 +40,7 @@ public static class cce { /// <param name="nullability">If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>!</param>
/// <returns></returns>
[Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
+ public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) where T : class {
return (nullability && collection == null) || cce.NonNullElements(collection);
//Should be the same as:
/*if(nullability&&collection==null)
@@ -50,11 +50,11 @@ public static class cce { }
[Pure]
- public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
+ public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) where TKey : class where TValue : class {
return kvp.Key != null && kvp.Value != null;
}
[Pure]
- public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
+ public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) where T : class {
return iEnumerator != null;
}
//[Pure]
@@ -135,6 +135,7 @@ public static class cce { //internal static bool NonNullElements(Set set) {
// return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
//}
+
}
public class PeerAttribute : SA {
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;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d2536aa4..a8acb013 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 59a1331d..82cb6651 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/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/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs index a3337ccc..9f4b22c5 100644 --- a/Source/Dafny/SccGraph.cs +++ b/Source/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/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 6c1deb12..b641b69d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/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/Source/Dafny/cce.cs b/Source/Dafny/cce.cs index 8391361b..ff5152d0 100644 --- a/Source/Dafny/cce.cs +++ b/Source/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]
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index aa0be9dd..91e33ea9 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -332,7 +332,7 @@ namespace Microsoft.Boogie static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName,
out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)
{Contract.Requires(program != null);
- Contract.Requires(cce.NonNullElements(bplFileName));
+ Contract.Requires(bplFileName != null);
Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index bc256cd5..8c01d8db 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -33,7 +33,8 @@ namespace Graphing { foreach (KeyValuePair<Node, List<Node>> de in d) {
if (!first)
sb.Append(", ");
- sb.Append(cce.NonNull(de.Key).ToString());
+ Contract.Assert(!object.Equals(de.Key,default(Node)));
+ sb.Append(de.Key.ToString());
sb.Append("~>");
sb.Append(ListToString(de.Value));
first = false;
@@ -131,7 +132,8 @@ namespace Graphing { foreach (KeyValuePair<Node, List<Node>> de in domMap) {
if (!first)
sb.Append(", ");
- sb.Append(cce.NonNull(de.Key).ToString());
+ Contract.Assert(!object.Equals(de.Key, default(Node)));
+ sb.Append(de.Key.ToString());
sb.Append("~>");
sb.Append(ListToString(de.Value));
first = false;
diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.cs b/Source/Provers/Simplify/Let2ImpliesVisitor.cs index 960a0a8d..9b8328d1 100644 --- a/Source/Provers/Simplify/Let2ImpliesVisitor.cs +++ b/Source/Provers/Simplify/Let2ImpliesVisitor.cs @@ -80,7 +80,7 @@ namespace Microsoft.Boogie.Simplify [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(VarOccurrences));
+ Contract.Invariant(VarOccurrences != null);
}
////////////////////////////////////////////////////////////////////////////
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 2645838d..68c02c5d 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -209,7 +209,7 @@ namespace Microsoft.Boogie.Simplify { [ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(BackgroundPredicates));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(BackgroundPredicates));
Contract.Invariant(BackgroundPredFilename != null);
Contract.Invariant(ctx != null);
}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index c2bb7500..83294381 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -456,7 +456,7 @@ namespace Microsoft.Boogie.Z3 {
Contract.Requires(partitionToValue != null);
Contract.Requires(valueToPartition != null);
- Contract.Requires(cce.NonNullElements(identifierToPartition));
+ Contract.Requires(identifierToPartition != null);
Contract.Requires(cce.NonNullElements(partitionToIdentifiers));
Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
string s = FromReadLine();
@@ -511,7 +511,7 @@ namespace Microsoft.Boogie.Z3 } else if (s[j] == '{') {
// array
List<List<int>/*!*/> arrayModel = new List<List<int>/*!*/>();
- Contract.Assert(Contract.ForAll(arrayModel, a => cce.NonNullElements(a)));
+ Contract.Assert(Contract.ForAll(arrayModel, a => a != null));
string array = s.Substring(j + 1);
int index1, index2;
string from, to;
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs index cd01e325..303a0066 100644 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ b/Source/Provers/Z3/TypeDeclCollector.cs @@ -29,12 +29,12 @@ void ObjectInvariant() Contract.Invariant(Namer!=null);
Contract.Invariant(AllDecls != null);
Contract.Invariant(IncDecls != null);
- Contract.Invariant(cce.NonNullElements(KnownFunctions));
- Contract.Invariant(cce.NonNullElements(KnownVariables));
- Contract.Invariant(cce.NonNullElements(KnownTypes));
- Contract.Invariant(cce.NonNullElements(KnownBvOps));
- Contract.Invariant(cce.NonNullElements(KnownSelectFunctions));
- Contract.Invariant(cce.NonNullElements(KnownStoreFunctions));
+ Contract.Invariant(KnownFunctions != null);
+ Contract.Invariant(KnownVariables != null);
+ Contract.Invariant(KnownTypes != null);
+ Contract.Invariant(KnownBvOps != null);
+ Contract.Invariant(KnownSelectFunctions != null);
+ Contract.Invariant(KnownStoreFunctions != null);
}
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;
diff --git a/Source/VCExpr/Clustering.cs b/Source/VCExpr/Clustering.cs index 0f08c98e..1efc3606 100644 --- a/Source/VCExpr/Clustering.cs +++ b/Source/VCExpr/Clustering.cs @@ -25,8 +25,8 @@ namespace Microsoft.Boogie.Clustering { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Gen != null);
- Contract.Invariant(cce.NonNullElements(GlobalVariables));
- Contract.Invariant(cce.NonNullElements(SubtermClusters));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalVariables));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(SubtermClusters));
}
@@ -117,7 +117,7 @@ namespace Microsoft.Boogie.Clustering { void ObjectInvariant() {
Contract.Invariant(Op != null);
Contract.Invariant(Gen != null);
- Contract.Invariant(cce.NonNullElements(GlobalVariables));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalVariables));
}
// variables that are global and treated like constants
private readonly IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ GlobalVariables;
@@ -125,7 +125,7 @@ namespace Microsoft.Boogie.Clustering { private readonly VCExpressionGenerator/*!*/ Gen;
public TermClustersSameHead(VCExprOp op, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, VCExpressionGenerator/*!*/ gen) {
- Contract.Requires(cce.NonNullElements(globalVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));
Contract.Requires(gen != null);
Contract.Requires(op != null);
Op = op;
@@ -207,7 +207,7 @@ namespace Microsoft.Boogie.Clustering { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Gen != null);
- Contract.Invariant(cce.NonNullElements(GlobalVariables));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalVariables));
Contract.Invariant(Clusters != null);
Contract.Invariant(RemainingClusters != null);
Contract.Invariant(Distances != null);
@@ -220,7 +220,7 @@ namespace Microsoft.Boogie.Clustering { public Distance(Cluster a, Cluster b, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, VCExpressionGenerator gen) {
Contract.Requires(gen != null);
- Contract.Requires(cce.NonNullElements(globalVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));
AntiUnificationVisitor/*!*/ visitor = new AntiUnificationVisitor(gen);
Generator = (VCExprNAry)visitor.AntiUnify(a.Generator, b.Generator);
@@ -233,7 +233,7 @@ namespace Microsoft.Boogie.Clustering { public ClusteringMatrix(List<Cluster> clusters, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, VCExpressionGenerator gen) {
Contract.Requires(gen != null);
Contract.Requires(clusters != null);
- Contract.Requires(cce.NonNullElements(globalVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));
List<Cluster> c = new List<Cluster>();
c.AddRange(clusters);
Clusters = c;
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie.Clustering { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Gen != null);
- Contract.Invariant(cce.NonNullElements(Representation));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(Representation));
}
@@ -397,7 +397,7 @@ namespace Microsoft.Boogie.Clustering { }
public bool RepresentationIsRenaming(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars) {
- Contract.Requires(cce.NonNullElements(globalVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));
if (!Contract.ForAll(Representation, pair => pair.Key.Expr0 is VCExprVar && pair.Key.Expr1 is VCExprVar && !globalVars.ContainsKey(cce.NonNull((VCExprVar)pair.Key.Expr0)) && !globalVars.ContainsKey(cce.NonNull((VCExprVar/*!*/)pair.Key.Expr1))))
return false;
// check that all substituted variables are distinct
@@ -407,12 +407,12 @@ namespace Microsoft.Boogie.Clustering { }
public void RepresentationSize(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars, out int expr0Size, out int expr1Size) {
- Contract.Requires(cce.NonNullElements(globalVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));
ReprSizeComputingVisitor/*!*/ size0Visitor = new ReprSizeComputingVisitor();
ReprSizeComputingVisitor/*!*/ size1Visitor = new ReprSizeComputingVisitor();
foreach (KeyValuePair<ExprPair, VCExprVar/*!*/> pair in Representation) {
- Contract.Assert(cce.NonNullElements(pair));
+ Contract.Assert(pair.Value != null);
size0Visitor.ComputeSize(pair.Key.Expr0, globalVars);
size1Visitor.ComputeSize(pair.Key.Expr1, globalVars);
}
@@ -505,7 +505,7 @@ Contract.Ensures(Contract.Result<VCExprVar>() != null); public void ComputeSize(VCExpr expr, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars) {
Contract.Requires(expr != null);
- Contract.Requires(cce.NonNullElements(globalVars));
+ Contract.Requires(cce.NonNullDictionaryAndValues(globalVars));
Traverse(expr, globalVars);
}
diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs index 7c06af18..f811461d 100644 --- a/Source/VCExpr/NameClashResolver.cs +++ b/Source/VCExpr/NameClashResolver.cs @@ -58,12 +58,12 @@ namespace Microsoft.Boogie.VCExprAST { private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;
[ContractInvariantMethod]
void GlobalNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(GlobalNames));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalNames));
}
private readonly List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ LocalNames;
[ContractInvariantMethod]
void LocalNamesInvariantMethod() {
- Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullElements(i)));
+ Contract.Invariant(Contract.ForAll(LocalNames, i => i != null && cce.NonNullDictionaryAndValues(i)));
}
// dictionary of all names that have already been used
@@ -71,17 +71,17 @@ namespace Microsoft.Boogie.VCExprAST { private readonly IDictionary<string/*!*/, bool/*!*/>/*!*/ UsedNames;
[ContractInvariantMethod]
void UsedNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(UsedNames));
+ Contract.Invariant(UsedNames != null);
}
private readonly IDictionary<string/*!*/, int/*!*/>/*!*/ CurrentCounters;
[ContractInvariantMethod]
void CurrentCountersInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(CurrentCounters));
+ Contract.Invariant(CurrentCounters != null);
}
private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalPlusLocalNames;
[ContractInvariantMethod]
void GlobalPlusLocalNamesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(GlobalPlusLocalNames));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(GlobalPlusLocalNames));
}
////////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 5f3dbc36..616575db 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -74,7 +74,7 @@ namespace Microsoft.Boogie.TypeErasure { return arguments;
}
- public static List<T/*!*/>/*!*/ ToList<T>(params T[] args) {
+ public static List<T/*!*/>/*!*/ ToList<T>(params T[] args) where T : class{
Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<T>>()));
return new List<T>(args);
@@ -335,7 +335,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<Type/*!*/, VCExpr/*!*/>/*!*/ BasicTypeReprs;
[ContractInvariantMethod]
void BasicTypeReprsInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(BasicTypeReprs));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(BasicTypeReprs));
}
private VCExpr GetBasicTypeRepr(Type type) {
@@ -354,7 +354,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<TypeCtorDecl/*!*/, TypeCtorRepr/*!*/>/*!*/ TypeCtorReprs;
[ContractInvariantMethod]
void TypeCtorReprsInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(TypeCtorReprs));
+ Contract.Invariant(TypeCtorReprs != null);
}
internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl decl) {
@@ -395,7 +395,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<TypeVariable/*!*/, VCExprVar/*!*/>/*!*/ TypeVariableMapping;
[ContractInvariantMethod]
void TypeVariableMappingInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(TypeVariableMapping));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableMapping));
}
public VCExprVar Typed2Untyped(TypeVariable var) {
@@ -417,7 +417,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ Typed2UntypedVariables;
[ContractInvariantMethod]
void Typed2UntypedVariablesInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(Typed2UntypedVariables));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedVariables));
}
// This method must only be used for free (unbound) variables
@@ -457,7 +457,7 @@ namespace Microsoft.Boogie.TypeErasure { public VCExpr Type2Term(Type type, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
Contract.Requires(type != null);
- Contract.Requires(cce.NonNullElements(varMapping));
+ Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));
Contract.Ensures(Contract.Result<VCExpr>() != null);
//
if (type.IsBasic || type.IsBv) {
@@ -654,7 +654,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<Type/*!*/, TypeCastSet/*!*/>/*!*/ TypeCasts;
[ContractInvariantMethod]
void TypeCastsInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(TypeCasts));
+ Contract.Invariant(TypeCasts != null);
}
private TypeCastSet GetTypeCasts(Type type) {
@@ -911,7 +911,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<MapType/*!*/, MapTypeClassRepresentation/*!*/>/*!*/ ClassRepresentations;
[ContractInvariantMethod]
void ClassRepresentationsInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(ClassRepresentations));
+ Contract.Invariant(ClassRepresentations != null);
}
protected MapTypeClassRepresentation GetClassRepresentation(MapType abstractedType) {
@@ -1062,15 +1062,15 @@ namespace Microsoft.Boogie.TypeErasure { public readonly IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ TypeVariableBindings;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(VCExprVarBindings));
- Contract.Invariant(cce.NonNullElements(TypeVariableBindings));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(VCExprVarBindings));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableBindings));
}
public VariableBindings(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ vcExprVarBindings,
IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ typeVariableBindings) {
- Contract.Requires(cce.NonNullElements(vcExprVarBindings));
- Contract.Requires(cce.NonNullElements(typeVariableBindings));
+ Contract.Requires(cce.NonNullDictionaryAndValues(vcExprVarBindings));
+ Contract.Requires(cce.NonNullDictionaryAndValues(typeVariableBindings));
this.VCExprVarBindings = vcExprVarBindings;
this.TypeVariableBindings = typeVariableBindings;
}
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index 6cc021fa..8187fa10 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -96,7 +96,7 @@ namespace Microsoft.Boogie.TypeErasure { private readonly IDictionary<Function/*!*/, Function/*!*/>/*!*/ Typed2UntypedFunctions;
[ContractInvariantMethod]
void Typed2UntypedFunctionsInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedFunctions));
}
public Function Typed2Untyped(Function fun) {
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index 25aa8074..b20fa143 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -332,7 +332,7 @@ namespace Microsoft.Boogie.TypeErasure private readonly IDictionary<Function/*!*/, UntypedFunction/*!*/>/*!*/ Typed2UntypedFunctions;
[ContractInvariantMethod]
void Typed2UntypedFunctionsInvariantMethod() {
- Contract.Invariant(cce.NonNullElements(Typed2UntypedFunctions));
+ Contract.Invariant(Typed2UntypedFunctions != null);
}
// distinguish between implicit and explicit type parameters
@@ -509,7 +509,7 @@ namespace Microsoft.Boogie.TypeErasure public VCExpr GenVarTypeAxiom(VCExprVar var, Type originalType, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
Contract.Requires(var != null);
Contract.Requires(originalType != null);
- Contract.Requires(cce.NonNullElements(varMapping));
+ Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));
Contract.Ensures(Contract.Result<VCExpr>() != null);
if (!var.Type.Equals(originalType)) {
@@ -583,7 +583,7 @@ namespace Microsoft.Boogie.TypeErasure new Dictionary<MapType/*!*/, List<int>/*!*/>();
[ContractInvariantMethod]
void ObjectInvarant() {
- Contract.Invariant(cce.NonNullElements(explicitSelectTypeParamsCache));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(explicitSelectTypeParamsCache));
}
@@ -1039,7 +1039,7 @@ namespace Microsoft.Boogie.TypeErasure out List<VCTrigger/*!*/>/*!*/ triggers) {
Contract.Requires(cce.NonNullElements(oldBoundVars));
Contract.Requires(cce.NonNullElements(newBoundVars));
- Contract.Requires(cce.NonNullElements(typeVarTranslation));
+ Contract.Requires(cce.NonNullDictionaryAndValues(typeVarTranslation));
Contract.Requires(cce.NonNullElements(typeVarBindings));
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out triggers)));
Contract.Ensures(Contract.Result<VCExpr>() != null);
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)
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 344d795b..3d407150 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -419,8 +419,8 @@ namespace Microsoft.Boogie.VCExprAST { new Dictionary<VCExprVar/*!*/, int>();
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(BoundTermVarsDict));
- Contract.Invariant(cce.NonNullElements(BoundTypeVarsDict));
+ Contract.Invariant(BoundTermVarsDict != null);
+ Contract.Invariant(BoundTypeVarsDict != null);
}
private readonly IDictionary<TypeVariable/*!*/, int>/*!*/ BoundTypeVarsDict =
@@ -441,7 +441,7 @@ namespace Microsoft.Boogie.VCExprAST { private void AddBoundVar<T>(IDictionary<T, int> dict, T sym) {
Contract.Requires(sym != null);
- Contract.Requires(cce.NonNullElements(dict));
+ Contract.Requires(dict != null);
int n;
if (dict.TryGetValue(sym, out n))
dict[sym] = n + 1;
@@ -451,7 +451,7 @@ namespace Microsoft.Boogie.VCExprAST { private void RemoveBoundVar<T>(IDictionary<T/*!*/, int/*!*/>/*!*/ dict, T sym) {
Contract.Requires(sym != null);
- Contract.Requires(cce.NonNullElements(dict));
+ Contract.Requires(dict != null);
int n;
bool b = dict.TryGetValue(sym, out n);
Contract.Assert(b && n > 0);
@@ -969,17 +969,17 @@ namespace Microsoft.Boogie.VCExprAST { private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;
[ContractInvariantMethod]
void TermSubstsInvariantMethod() {
- Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));
+ Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullDictionaryAndValues(i)));
}
private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;
[ContractInvariantMethod]
void TypeSubstsInvariantMethod() {
- Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));
+ Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullDictionaryAndValues(i)));
}
public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {
- Contract.Requires(cce.NonNullElements(termSubst));
- Contract.Requires(cce.NonNullElements(typeSubst));
+ Contract.Requires(cce.NonNullDictionaryAndValues(termSubst));
+ Contract.Requires(cce.NonNullDictionaryAndValues(typeSubst));
List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ termSubsts =
new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>();
termSubsts.Add(termSubst);
@@ -1059,7 +1059,7 @@ namespace Microsoft.Boogie.VCExprAST { public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {
get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));
+ Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {
@@ -1232,7 +1232,7 @@ namespace Microsoft.Boogie.VCExprAST { // right types
boundVars = new List<VCExprVar/*!*/>();
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
- Contract.Assert(cce.NonNullElements(typeSubst));
+ Contract.Assert(cce.NonNullDictionaryAndValues(typeSubst));
foreach (VCExprVar/*!*/ var in node.BoundVars) {
Contract.Assert(var != null);
VCExprVar/*!*/ freshVar =
@@ -1302,7 +1302,7 @@ namespace Microsoft.Boogie.VCExprAST { // right types
newBoundVars = new List<VCExprVar/*!*/>();
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
- Contract.Assert(cce.NonNullElements(typeSubst));
+ Contract.Assert(cce.NonNullDictionaryAndValues(typeSubst));
foreach (VCExprVar/*!*/ var in node.BoundVars) {
Contract.Assert(var != null);
VCExprVar/*!*/ freshVar =
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 5618fafa..119218a1 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -336,22 +336,22 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(identifierToPartition));
+ Contract.Invariant(identifierToPartition != null);
Contract.Invariant(partitionToIdentifiers != null);
Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
Contract.Invariant(partitionToValue != null);
Contract.Invariant(valueToPartition != null);
- Contract.Invariant(cce.NonNullElements(definedFunctions));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(definedFunctions));
}
public ErrorModel(Dictionary<string, int> identifierToPartition, List<List<string>> partitionToIdentifiers, List<Object> partitionToValue, Dictionary<object, int> valueToPartition, Dictionary<string, List<List<int>>> definedFunctions) {
- Contract.Requires(cce.NonNullElements(identifierToPartition));
+ Contract.Requires(identifierToPartition != null);
Contract.Requires(partitionToIdentifiers != null);
Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
Contract.Requires(partitionToValue != null);
Contract.Requires(valueToPartition != null);
- Contract.Requires(cce.NonNullElements(definedFunctions));
+ Contract.Requires(cce.NonNullDictionaryAndValues(definedFunctions));
this.identifierToPartition = identifierToPartition;
this.partitionToIdentifiers = partitionToIdentifiers;
this.partitionToValue = partitionToValue;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 20b17e6b..6400aaf2 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -71,7 +71,7 @@ namespace Microsoft.Boogie { Contract.Invariant(Trace != null);
Contract.Invariant(Context != null);
Contract.Invariant(cce.NonNullElements(relatedInformation));
- Contract.Invariant(cce.NonNullElements(calleeCounterexamples));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples));
}
[Peer]
@@ -112,7 +112,7 @@ namespace Microsoft.Boogie { public void AddCalleeCounterexample(Dictionary<TraceLocation, CalleeCounterexampleInfo> cs)
{
- Contract.Requires(cce.NonNullElements(cs));
+ Contract.Requires(cce.NonNullDictionaryAndValues(cs));
foreach (TraceLocation loc in cs.Keys)
{
AddCalleeCounterexample(loc, cs[loc]);
@@ -474,7 +474,7 @@ namespace VC { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(checkers));
- Contract.Invariant(cce.NonNullElements(incarnationOriginMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Invariant(program != null);
}
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs index 8a9f808c..03f0af8f 100644 --- a/Source/VCGeneration/DoomCheck.cs +++ b/Source/VCGeneration/DoomCheck.cs @@ -717,7 +717,7 @@ void ObjectInvariant() #region Collect Unavoidable Blocks
private Block BreadthFirst(Block start, Dictionary<Block, TraceNode> blockmap) {
Contract.Requires(start != null);
- Contract.Requires(cce.NonNullElements(blockmap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(blockmap));
Contract.Ensures(Contract.Result<Block>() != null);
List<Block> JobList = new List<Block>();
@@ -800,7 +800,7 @@ void ObjectInvariant() // it should be implemented using one function later on.
private void BreadthFirstBwd(Block start, Dictionary<Block, TraceNode> blockmap) {
Contract.Requires(start != null);
- Contract.Requires(cce.NonNullElements(blockmap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(blockmap));
List<Block> JobList = new List<Block>();
List<Block> DoneList = new List<Block>();
diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs index 877fba13..4fbc80da 100644 --- a/Source/VCGeneration/OrderingAxioms.cs +++ b/Source/VCGeneration/OrderingAxioms.cs @@ -24,7 +24,7 @@ namespace Microsoft.Boogie { void ObjectInvariant() {
Contract.Invariant(Gen != null);
Contract.Invariant(Translator != null);
- Contract.Invariant(cce.NonNullElements(OneStepFuns));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(OneStepFuns));
Contract.Invariant(cce.NonNullElements(Constants));
Contract.Invariant(cce.NonNullElements(CompleteConstantsOpen));
Contract.Invariant(cce.NonNullElements(AllAxioms));
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index c418f828..48029154 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -26,7 +26,7 @@ namespace VC [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
}
/// <summary>
@@ -1675,12 +1675,12 @@ namespace VC [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
Contract.Invariant(mainLabel2absy != null);
- Contract.Invariant(cce.NonNullElements(boogieExpr2Id));
- Contract.Invariant(cce.NonNullElements(id2Candidate));
- Contract.Invariant(cce.NonNullElements(id2ControlVar));
- Contract.Invariant(cce.NonNullElements(label2Id));
+ Contract.Invariant(boogieExpr2Id != null);
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2Candidate));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2ControlVar));
+ Contract.Invariant(label2Id != null);
}
// Name of the procedure whose VC we're mutating
@@ -1696,7 +1696,7 @@ namespace VC : base(gen)
{
Contract.Requires(gen != null);
- Contract.Requires(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
Contract.Requires(mainLabel2absy != null);
this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
this.mainProcName = mainProcName;
@@ -2023,7 +2023,7 @@ namespace VC [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(subst));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
}
@@ -2105,7 +2105,7 @@ namespace VC Contract.Invariant(program != null);
Contract.Invariant(callback != null);
Contract.Invariant(theoremProver != null);
- Contract.Invariant(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
}
@@ -2114,7 +2114,7 @@ namespace VC Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,
Program/*!*/ program, Implementation/*!*/ mainImpl)
{
- Contract.Requires(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
Contract.Requires(theoremProver != null);
Contract.Requires(callback != null);
Contract.Requires(context != null);
@@ -2268,7 +2268,7 @@ namespace VC Contract.Requires(b != null);
Contract.Requires(traceNodes != null);
Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullElements(calleeCounterexamples));
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
while (true)
{
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 0215784b..1062767c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -73,7 +73,7 @@ namespace VC { Contract.Invariant(controlFlowVariable != null);
Contract.Invariant(assertExpr != null);
Contract.Invariant(cce.NonNullElements(interfaceVars));
- Contract.Invariant(incarnationOriginMap == null || cce.NonNullElements(incarnationOriginMap));
+ Contract.Invariant(incarnationOriginMap == null || cce.NonNullDictionaryAndValues(incarnationOriginMap));
}
public Implementation impl;
@@ -145,7 +145,7 @@ namespace VC { }
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
}
private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;
@@ -283,8 +283,8 @@ namespace VC { Contract.Invariant(impl != null);
Contract.Invariant(initial != null);
Contract.Invariant(program != null);
- Contract.Invariant(cce.NonNullElements(copies));
- Contract.Invariant(cce.NonNullElements(visited));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(copies));
+ Contract.Invariant(visited != null);
Contract.Invariant(callback != null);
}
@@ -690,14 +690,14 @@ namespace VC { void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(blocks));
Contract.Invariant(cce.NonNullElements(big_blocks));
- Contract.Invariant(cce.NonNullElements(stats));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(stats));
Contract.Invariant(cce.NonNullElements(assumized_branches));
Contract.Invariant(gotoCmdOrigins != null);
Contract.Invariant(parent != null);
Contract.Invariant(impl != null);
Contract.Invariant(copies != null);
- Contract.Invariant(cce.NonNullElements(protected_from_assert_to_assume));
- Contract.Invariant(cce.NonNullElements(keep_at_all));
+ Contract.Invariant(protected_from_assert_to_assume != null);
+ Contract.Invariant(keep_at_all != null);
}
@@ -863,7 +863,7 @@ namespace VC { Dictionary<Block/*!*/, bool>/*!*/ ComputeReachableNodes(Block/*!*/ b) {
Contract.Requires(b != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<Block, bool>>()));
+ Contract.Ensures(Contract.Result<Dictionary<Block, bool>>() != null);
BlockStats s = GetBlockStats(b);
if (s.reachable_blocks != null) {
return s.reachable_blocks;
@@ -1462,7 +1462,7 @@ namespace VC { }
private void SoundnessCheck(Dictionary<PureCollections.Tuple/*!*/, bool>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
- Contract.Requires(cce.NonNullElements(cache));
+ Contract.Requires(cache != null);
Contract.Requires(orig != null);
Contract.Requires(copies != null);
{
@@ -1758,9 +1758,9 @@ namespace VC { Contract.Invariant(gotoCmdOrigins != null);
Contract.Invariant(label2absy != null);
Contract.Invariant(cce.NonNullElements(blocks));
- Contract.Invariant(cce.NonNullElements(incarnationOriginMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Invariant(callback != null);
- Contract.Invariant(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Invariant(context != null);
Contract.Invariant(program != null);
}
@@ -1792,9 +1792,9 @@ namespace VC { Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(label2absy != null);
Contract.Requires(cce.NonNullElements(blocks));
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context!=null);
Contract.Requires(program!=null);
this.gotoCmdOrigins = gotoCmdOrigins;
@@ -1893,9 +1893,9 @@ namespace VC { Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(label2absy != null);
Contract.Requires(cce.NonNullElements(blocks));
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
}
@@ -2534,7 +2534,7 @@ namespace VC { string/*!*/ implName, List<int>/*!*/ values)
{
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
Contract.Requires(implName != null);
@@ -2662,7 +2662,7 @@ namespace VC { Contract.Requires(b != null);
Contract.Requires(trace != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
// After translation, all potential errors come from asserts.
return null;
@@ -2678,11 +2678,11 @@ namespace VC { Contract.Requires(b != null);
Contract.Requires(traceNodes != null);
Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
- Contract.Requires(cce.NonNullElements(calleeCounterexamples));
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
CmdSeq cmds = b.Cmds;
Contract.Assert(cmds != null);
@@ -2762,9 +2762,9 @@ namespace VC { Contract.Requires(expr != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(exprToPrintableValue));
+ Contract.Requires(cce.NonNullDictionaryAndValues(exprToPrintableValue));
Contract.Requires(cce.NonNullElements(relatedInformation));
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
if (errorDataEnhanced is ListOfMiningStrategies) {
ListOfMiningStrategies loms = (ListOfMiningStrategies)errorDataEnhanced;
List < MiningStrategy > l = loms.msList;
@@ -2842,7 +2842,7 @@ namespace VC { Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap, List<string/*!*/>/*!*/ relatedInformation) {
Contract.Requires(incarnationMap != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(cce.NonNullElements(relatedInformation));
List<int> heapSuccList = ComputeHeapSuccessions(incarnationMap, errModel);
TreatHeapSuccessions(heapSuccList, incarnationMap, errModel, incarnationOriginMap, relatedInformation);
@@ -2971,7 +2971,7 @@ namespace VC { Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap, List<string/*!*/>/*!*/ relatedInformation) {
Contract.Requires(incarnationMap != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(cce.NonNullElements(relatedInformation));
if (heapSuccessionList == null) {
// empty list of heap successions, nothing we can do!
@@ -3469,7 +3469,7 @@ namespace VC { Contract.Requires(transferCmd != null);
Contract.Requires(trace != null);
Contract.Requires(context != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Ensures(Contract.Result<Counterexample>() != null);
List<string> relatedInformation = new List<string>();
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index c0d3ac68..950c0158 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -25,8 +25,8 @@ namespace VC { List<Cmd/*!*/>/*!*/ m_doomedCmds = new List<Cmd/*!*/>();
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(m_BlockReachabilityMap));
- Contract.Invariant(cce.NonNullElements(m_copiedBlocks));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(m_BlockReachabilityMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(m_copiedBlocks));
Contract.Invariant(cce.NonNullElements(m_doomedCmds));
Contract.Invariant(cce.NonNullElements(_copiedBlock));
}
@@ -95,10 +95,10 @@ namespace VC { private Block CopyImplBlocks(Block b, ref List<Block> blocklist, Block targetBlock, ref Dictionary<Block, Block> alreadySeen) {
Contract.Requires(b != null);
Contract.Requires(targetBlock != null);
- Contract.Requires(cce.NonNullElements(alreadySeen));
+ Contract.Requires(cce.NonNullDictionaryAndValues(alreadySeen));
Contract.Requires(blocklist != null);
Contract.Ensures(Contract.ValueAtReturn(out blocklist) != null);
- Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out alreadySeen)));
+ Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.ValueAtReturn(out alreadySeen)));
Contract.Ensures(Contract.Result<Block>() != null);
Block seen;
@@ -635,7 +635,7 @@ namespace VC { Contract.Requires(reachvar != null);
Contract.Requires(impl != null);
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullElements(cmdbackup));
+ Contract.Requires(cce.NonNullDictionaryAndValues(cmdbackup));
#region Modify implementation
for (int i = startidx; i <= endidx; i++) {
if (_copiedBlock.Contains(impl.Blocks[i]))
@@ -762,7 +762,7 @@ namespace VC { void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,
int startidx, int endidx) {
- Contract.Requires(cce.NonNullElements(cmdbackup));
+ Contract.Requires(cce.NonNullDictionaryAndValues(cmdbackup));
Contract.Requires(impl != null);
for (int i = startidx; i <= endidx; i++) {
CmdSeq cs = null;
@@ -832,7 +832,7 @@ namespace VC { void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Blocks));
Contract.Invariant(cce.NonNullElements(m_checkableBlocks));
- Contract.Invariant(cce.NonNullElements(m_copyMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(m_copyMap));
}
@@ -868,7 +868,7 @@ namespace VC { private Block AbstractLoopUnrolling(GraphNode node, Dictionary<GraphNode, Block> visited, bool unrollable, String prefix)
{
Contract.Requires(node != null);
- Contract.Requires(cce.NonNullElements(visited));
+ Contract.Requires(cce.NonNullDictionaryAndValues(visited));
Contract.Requires(prefix != null);
Contract.Ensures(Contract.Result<Block>() != null);
Block newb;
@@ -1207,7 +1207,7 @@ namespace VC { public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block, GraphNode> gd, Set /*Block*/ beingVisited) {
Contract.Requires(b != null);
Contract.Requires(beingVisited != null);
- Contract.Requires(cce.NonNullElements(gd));
+ Contract.Requires(cce.NonNullDictionaryAndValues(gd));
Contract.Ensures(Contract.Result<GraphNode>() != null);
|