"Invariant unproven" when using method that creates a specific new object in its return statement

Question

The following simple code will yield an "invariant unproven" warning by the static checker of Code Contracts, although there is no way _foo can be null. The warning is for the return statement inside UncalledMethod.

public class Node
{
    public Node(string s1, string s2, string s3, string s4, object o,
                string s5)
    {
    }
}

public class Bar
{
    private readonly string _foo;

    public Bar()
    {
        _foo = "foo";
    }

    private object UncalledMethod()
    {
        return new Node(string.Empty, string.Empty, string.Empty, string.Empty,
                        GetNode(), string.Empty);
    }

    private Node GetNode()
    {
        return null;
    }

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

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

Apart from the fact, that the warning is simply invalid, it only occures in certain specific circumstances. Changing any of the following will make the warning go away:

1. Inline GetNode so the return statement looks like this:

   return new Node(string.Empty, string.Empty, string.Empty, string.Empty, null,
                   string.Empty);
   

2. Remove any of the parameters s1 to s5 from the constructor of Node.
3. Change the type of any of the parameters s1 to s5 from the constructor of Node to object.

4. Use a temporary variable for the result of GetNode:

       var node = GetNode();
       return new Node(string.Empty, string.Empty, string.Empty, string.Empty,
                       node, string.Empty);
   

5. Changing the order of the parameters of the constructor of Node.
6. Checking the option "Show assumptions" in the code contracts settings pane in the project settings.

Am I missing something obvious here or is this simply a bug in the static checker?

---

My settings:

My output:

C:\{path}\Program.cs(20,9): message : CodeContracts: Suggested ensures: Contract.Ensures(this._foo != null);
C:\{path}\Program.cs(41,17): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.String>() == this._foo);
C:\{path}\Program.cs(33,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<ConsoleApplication3.Program+Node>() == null);
C:\{path}\Program.cs(27,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Result<System.Object>() != null);
C:\{path}\Program.cs(55,13): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, args.Length, __k__ => args[__k__] != 0));
CodeContracts: ConsoleApplication3: Validated:  92,3%
CodeContracts: ConsoleApplication3: Contract density: 1,81
CodeContracts: ConsoleApplication3: Total methods analyzed 8
CodeContracts: ConsoleApplication3: Methods with 0 warnings 7
CodeContracts: ConsoleApplication3: Total method analysis read from the cache 8
CodeContracts: ConsoleApplication3: Total time 2,522sec. 315ms/method
CodeContracts: ConsoleApplication3: Retained 0 preconditions after filtering
CodeContracts: ConsoleApplication3: Inferred 0 object invariants
CodeContracts: ConsoleApplication3: Retained 0 object invariants after filtering
CodeContracts: ConsoleApplication3: Detected 0 code fixes
CodeContracts: ConsoleApplication3: Proof obligations with a code fix: 0
C:\{path}\Program.cs(27,13): warning : CodeContracts: invariant unproven: _foo != null
C:\{path}\Program.cs(49,13): warning :   + location related to previous warning
C:\windows\system32\ConsoleApplication3.exe(1,1): message : CodeContracts: Checked 13 assertions: 12 correct 1 unknown
CodeContracts: ConsoleApplication3: 
CodeContracts: ConsoleApplication3: Background contract analysis done.

Answer 1

This is no longer a problem with the latest version.