Bug: Side-effects concluded for null-coalescing operator

Question

The static verifier seems to conclude that a use of the null-coalescing operator can have side-effects. For the Foo class below it generates the following warning related to the post-condition of the constructor: warning CC1069: CodeContracts: Detected expression statement evaluated for potential side-effect in contracts of method 'CodeContractsBug.Foo.#ctor(System.String)'. (Did you mean to put the expression into a Requires, Ensures, or Invariant call?). In my real project it becomes a compile-time error (error CC1069) because runtime contract checking is enabled.

    public class Foo
    {
        private readonly string _bar;

        public string Bar
        {
            get
            {
                Contract.Ensures(Contract.Result<string>() != null);
                return _bar;
            }
        }

        public Foo(string bar = null)
        {
            Contract.Ensures(Bar == (bar ?? string.Empty));
            _bar = bar ?? string.Empty;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(_bar != null);
        }
    }

Replacing the post-condition with the following line eliminates the warning:

Contract.Ensures(Bar == (bar != null ? bar : string.Empty));

Is this a bug or am I missing some finer language detail?

I am using version 1.4.51019.0 with VS 2010.

Answer 1

Hi,

I was able to repro in VS 2012.  It does seem like a bug.  The null-coalescing operator itself is certainly pure, and so are both operands in your example.

- Dave

---

http://davesexton.com/blog

Answer 2

Yup, we are overly eager at marking things as side effects. I fixed this problem and will push it out as soon as possible.

-MaF

---

Cheers, -MaF (Manuel Fahndrich)

Answer 3

The new release 1.4.60301.15 should fix this.

---

Cheers, -MaF (Manuel Fahndrich)