Merge pull request #201 from fedotovalex/fix-200

Corrected contracts of string.IndexOfAny(char[], ...)
microsoft · Aug 10, 2015 · 0fbc6e0 · 0fbc6e0
2 parents 270f54d + 8e67b6e
commit 0fbc6e0
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Microsoft.Research/Contracts/MsCorlib/System.String.cs b/Microsoft.Research/Contracts/MsCorlib/System.String.cs
@@ -779,7 +779,7 @@ public int IndexOfAny(char[] anyOf, int startIndex)
       Contract.Requires(anyOf != null);
 
       Contract.Requires(startIndex >= 0);
-      Contract.Requires(startIndex < Length);
+      Contract.Requires(startIndex <= Length);
 
       Contract.Ensures(-1 <= Contract.Result<int>());
       Contract.Ensures(Contract.Result<int>() < this.Length);
@@ -795,8 +795,7 @@ public int IndexOfAny(char[] anyOf, int startIndex, int count)
 
       Contract.Requires(startIndex >= 0);
       Contract.Requires(count >= 0);
-
-      Contract.Requires(startIndex + count < Length);
+      Contract.Requires(startIndex + count <= Length);
 
       Contract.Ensures(-1 <= Contract.Result<int>());
       Contract.Ensures(Contract.Result<int>() < this.Length);