Is Code Contracts failing to spot obvious relationship between Nullable<T>.HasValue and null?

Question

I am experimenting with applying Code Contracts to my code and I've hit a perplexing problem. This code is failing to meet the contract but unless I'm being really thick I would expect it to be able to easily analyse that id must have a value at the point of return

if (id == null)
    throw new InvalidOperationException(string.Format("{0} '{1}' does not yet have an identity", typeof(T).Name, entity));

return id.Value;

Answer 1

I've got to the bottom of this behaviour and it is not Code Contract's fault.

I opened the generated assembly in ILSpy and this is the code that is produced:

public Guid Id
{
    get
    {
        Guid? guid = this.id;
        if (!guid.HasValue)
        {
            throw new InvalidOperationException();
        }
        guid = this.id;
        return guid.Value;
    }
}

The instance variable id is being copied to a local variable and this local variable is being reset back to its original value after the condition block. Now it became obvious why Code Contracts is showing a contract violation error but it still left me confused why the code was being rewritten in this form. I did a little more experimentation and took Code Contracts out of the project altogether and it became apparent that this is standard C# compiler behaviour, but why?

The secret appears to be due to a minor detail that I accidentally omitted from my original question. The id instance variable is declared as readonly and this seems to be responsible for causing the compiler to add the temporary guid variable.

I must admit I'm still confused why the compiler feels it needs to do this to ensure the guarantee of immutability for id but I'll keep digging...

Answer 2

You might try copying the field to a local value and writing the statements in terms of that local value. The prover may be conservative about fields, since it's possible that a call could mutate the field value.