"Invariant unproven" quando si utilizza il metodo che crea un nuovo oggetto specifico nell'istruzione return

Question

Il seguente codice semplice produrrà un avviso "invariato non dimostrato" dal controllo statico dei Contratti di codice, sebbene non sia possibile che _foo possa essere null. L'avviso è per l'istruzione return all'interno di 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); 
    } 
} 

A parte il fatto, che l'avvertimento è semplicemente invalida, occures solo in determinate circostanze specifiche. La modifica qualsiasi delle seguenti renderà l'avvertimento andare via:

1. Inline GetNode così l'istruzione return è simile al seguente:

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

2. Rimuovere qualsiasi parametro s1 a s5 dal costruttore di Node.
3. Modificare il tipo di uno qualsiasi dei parametri da s1 a s5 dal costruttore di Node a object.

4. Utilizzare una variabile temporanea per il risultato di GetNode:

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

5. Cambiando l'ordine dei parametri del costruttore Node.
6. Controllare l'opzione "Mostra ipotesi" nel riquadro delle impostazioni del contratto di codice nelle impostazioni del progetto.

Mi manca qualcosa di ovvio qui o si tratta semplicemente di un errore nel controllo statico?

---

mie impostazioni:

mia uscita:

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

Questo non è più un problema con the latest version.