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

Viewed 275

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;

Code Contracts error: requires unproven: HasValue

3 Answers
Related