How can I specify code contracts for existing framework (BCL) code?

Code contracts work great until you have to add a bazillion Contract.Assume(...) for the results coming out of framework code. For instance, MemoryStream.ToArray() never returns a null array, as best as I can tell from looking at it in Reflector, but it'开发者_StackOverflow中文版s not documented as a contract, so I have to Assume it everywhere.

Is there a magical way to create a contract library for functions which already exist? I'm guessing that once you got a few dozen of the most commonly used framework functions contracted out, the warnings would get much more palatable.

I don't think you can directly. There are several things to do:

Request the contract be added in this thread on the Code Contracts forums.

The suggested workaround by the Code Contracts team for now is to make a static method that assumes all the contracts you need. I find that this works best with an extension method:

static class Contracted
{
    byte[] ToArrayContracted(this MemoryStream s)
    {
        Contract.Requires(s != null);
        Contract.Ensures(Contract.Result<byte[]>() != null);

        var result = s.ToArray();
        Contract.Assume(result != null);
        return result;
    }
}

This way, you use s.ToArrayContracted() instead of s.ToArray(), and once the contracts are available on the type, you can just search-and-replace ToArrayContracted to ToArray.