diff options
author | 2011-03-10 17:37:58 +0000 | |
---|---|---|
committer | 2011-03-10 17:37:58 +0000 | |
commit | 768ee8abb31d912cfdc8eeaf41d7f44f1691ce0c (patch) | |
tree | 533ab6aa0d91c5a5e7c66125834fb5b8695ccf71 /Source/Provers/Z3 | |
parent | e28c62b12194be07e3ecb3301e6b3e0336bcac2a (diff) |
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.
Diffstat (limited to 'Source/Provers/Z3')
-rw-r--r-- | Source/Provers/Z3/Prover.cs | 4 | ||||
-rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 12 |
2 files changed, 8 insertions, 8 deletions
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);
}
|