I'm not quite sure what cases the new suggestions are trying to cover, but it seems to be a result of the static analyser having a hard time with your ORed clause.
It's a good idea to keep the Contract.Requires
expressions as simple as possible, both to help the static analyser and to make it easier for human readers.
In this example, the following set of Requires
clauses doesn't cause any additional suggestions to be raised:
Contract.Requires(text != null);
Contract.Requires(array != null);
Contract.Requires(start >= 0);
Contract.Requires(start <= array.Length - length);
Contract.Requires(length >= 0);
These are stricter than your originals, but don't seem unreasonable for callers.
In particular, notice that start <= array.Length - length
is needed to prevent an array overflow on array[start + i]
; the original condition start < array.Length
is not sufficient, and might well be the root of your problem.
As an aside, if you're willing to use LINQ, you could rewrite this method more succinctly as follows:
static bool TextEquals2(string text, char[] array, int start, int length)
{
Contract.Requires(text != null);
Contract.Requires(array != null);
Contract.Requires(start >= 0);
Contract.Requires(length >= 0);
return text.SequenceEqual(array.Skip(start).Take(length));
}