Why is CodeContract warning about a null reference, when the ObjectInvariant checks it for null

Question

Am trying to get up to speed with Code Contracts. Here is another issue that doesn't make sense to me:

This is the Invariant:

[ContractInvariantMethod]
    void Invariant() {
        Contract.Invariant(this._uiRoot.RowDefinitions!=null);
    }

Then, in a Method is this code:

int colunmn = 0;
foreach (UIElement uiElement in row.Where(element => element!=null))
{
            if (uiElement != null)
            {
                uiElement.SetValue(Grid.ColumnProperty, colunmn++);
                uiElement.SetValue(Grid.RowProperty, _uiRoot.RowDefinitions.Count - 1);
                _uiRoot.Children.Add(uiElement);
            }
}

I then get a warning that _uiRoot.RowDefinitions may be null, despite the Invariant. I don't see why CodeContracts would think that if it is checked after every public method call and the constructor. The code in question is a custom form designer, and it uses the uiRoot.RowDefinitions in a number of different methods, which is why I wanted to put it into the Invariant. I thought this would be enough to stop the warnings on it.

Answer 1

I think invariant only runs on public property access. Is it possible to add a contract to the RowDefinitions property itself? Your invariant can't prove that property won't be null; you could call a method on that type which sets it to null after your invariant runs.