c# - returnステートメントで特定の新しいオブジェクトを作成するメソッドを使用する場合の「不変の証明されていない」

Question

次の単純なコードは、コードコントラクトの静的チェッカーによる「不変の証明されていない」警告を生成しますが、方法はありませ_fooんnull。警告は、return内のステートメントに対するもの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);
    }
}

警告が単に無効であるという事実は別として、それは特定の状況でのみ発生します。次のいずれかを変更すると、警告が消えます。

1. インラインGetNodeなので、returnステートメントは次のようになります。

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

2. のコンストラクターからパラメーターs1からs5のいずれかを削除しますNode。
3. パラメータs1からs5のいずれかのタイプをのコンストラクタからに変更Nodeしobjectます。

4. 次の結果には一時変数を使用しますGetNode。

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

5. のコンストラクターのパラメーターの順序を変更しますNode。
6. プロジェクト設定のコードコントラクト設定ペインで[前提条件を表示する]オプションをオンにします。

ここで明らかな何かが欠けていますか、それともこれは単に静的チェッカーのバグですか？

---

私の設定：

私の出力：

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

これは、最新バージョンでは問題ではなくなりました。