How to specify Ensures for out parameter?

Question

I have a method with an out parameter and I want to specify using Contract.Ensures() that when the method returns, the parameter will not be null.

Basically, this:

void M(out object o)
{
    Contract.Ensures(o != null);

    o = new object();
}

This does not compile, because it looks like the parameter will be read before it's assigned:

error CS0269: Use of unassigned out parameter 'o'

I thought I could fix this by switching the lines around, but that does not work either:

warning CC1005: CodeContracts: Malformed contract. Found Ensures after assignment in method 'M(System.Object@)'.

Is there some way to do this?

I don't want to switch the method to ref. I can't return the value instead of using out, because the actual method where I encountered this already has a return value: bool TryGetValue(TKey1 key1, TKey2 key2, out TValue value).

Answer 1

The Contract.ValueAtReturn method is available specifically to avoid the C# compiler's error here.

Contract.Ensures(Contract.ValueAtReturn(out o) != null);