summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/AbsyCmd.cs4
-rw-r--r--Source/Core/AbsyType.cs30
-rw-r--r--Source/Core/DeadVarElim.cs38
-rw-r--r--Source/Core/GraphAlgorithms.cs4
-rw-r--r--Source/Core/Inline.cs4
-rw-r--r--Source/Core/LoopUnroll.cs6
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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 22:31:57 +0000