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

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开发者_Python百科 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;

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...

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.

Its not seeing your if throw check as part of its contracts. Try this instead:

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

Contract.EndContractBlock();

http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.contract.endcontractblock.aspx