locked
Bug? Proving null from DataReader.FromBuffer() RRS feed

  • Question

  • public static void ContractBad(IBuffer left, IBuffer right)
            {
                Contract.Requires(left != null);
                Contract.Requires(right != null);
    
                using (var leftReader = DataReader.FromBuffer(left))
                using (var rightReader = DataReader.FromBuffer(right))
                {
                    leftReader.ReadByte();
                    rightReader.ReadByte();
                }
            }
            
            public static void ContractOkay(IBuffer left, IBuffer right)
            {
                if (ReferenceEquals(left, right))
                    return;
                else if (left == null || right == null)
                    return;
    
                using (var leftReader = DataReader.FromBuffer(left))
                using (var rightReader = DataReader.FromBuffer(right))
                {
                    leftReader.ReadByte();
                    rightReader.ReadByte();
                }
            }

    In the former method, I get contract null-dereference warnings on leftReader.ReadByte() and rightReader.ReadByte(). In the latter method, I don't. In fact, if I add Contract.Assume() within the using block for the readers != null, Contracts tells me that it can be replaced with an assert because it can be proven statically.

    Notably, in the latter method if I remove either guard statement, the null dereference warning re-appears. If I add a Requires(left != right) to the former method, the warning for that method disappears.

    But if I remove one of the readers completely, the warning comes back.

    Any idea what's happening here?

    Thursday, January 7, 2016 5:41 AM