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); 
    } 
} 

警告は単に無効であることを除けば、特定の状況でのみ発生します。以下のいずれかのを変更すると、警告が離れて行くようになります：のコンストラクタからS5に

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

は、パラメータs1のいずれかを削除します。

1. インラインGetNodeはそうreturn文は次のようになりますNode。

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

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

3. ：

4. はGetNodeの結果のために一時的な変数を使用してください。

5. プロジェクト設定の[コード契約]設定ウィンドウで[前提条件を表示]オプションをオンにします。

静的チェッカーのバグですか？

---

マイセッティング：

マイ出力：

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

これはもはやthe latest versionに問題はありません。