Code Contracts avvertono di "assicura non provata" quando le serrature sono coinvolti

Question

sto cercando di capire come i contratti di codice .NET interagiscono con la parola chiave lock, utilizzando il seguente esempio:

public class TestClass 
{ 
    private object o1 = new object(); 
    private object o2 = new object(); 

    private void Test() 
    { 
    Contract.Requires(this.o1 != null); 
    Contract.Requires(this.o2 != null); 
    Contract.Ensures(this.o1 != null); 

    lock (this.o2) { 
     this.o1 = new object(); 
    } 
    } 
} 

Quando eseguo lo strumento di analisi statica Codice contratto, esso stampa avvertimento aa: Ensures unproven: this.o1 != null

Se faccio qualsiasi:

• cambiamento del o2 nel lock a o1,
• modifica la o1 all'interno del lock blocco o2,
• aggiungendo una seconda linea all'interno del blocco lock assegnando un newobject per o2
• cambiamento lock (this.o2) a if (this.o2 != null),
• rimuovere la Dichiarazione lock interamente.

l'avviso scompare.

Tuttavia, cambiando la linea all'interno del lock blocco var temp = new object(); (eliminando in tal modo tutti i riferimenti al o1 dal metodo) provoca ancora l'avvertimento:

private void Test() 
    { 
    Contract.Requires(this.o1 != null); 
    Contract.Requires(this.o2 != null); 
    Contract.Ensures(this.o1 != null); 

    lock (this.o2) { 
     var temp = new object(); 
    } 
    } 

---

Quindi ci sono due domande:

1. Perché si verifica questo avviso?
2. Cosa si può fare per prevenirlo (tenendo presente che questo è un esempio di giocattolo e ci sono effettivamente cose che accadono all'interno dello lock nel codice reale)?

Answer 1

Ecco come il controllo statico tratta serrature e invarianti:

Se si blocca qualcosa con la serratura modulo (x.foo) {...}, il controllo statico considera x.foo come la serratura protegge di x . Alla fine dell'ambito del blocco, si presuppone che altri thread possano accedere a x e modificarlo. Di conseguenza, il controllo statico presuppone che tutti i campi di x soddisfino solo l'invarianza dell'oggetto dopo l'ambito del blocco, niente di più.

Si noti che questo non sta prendendo in considerazione tutti gli intrecci di filo, solo intrecci alla fine degli ambiti di blocco.

Answer 2

aggiungere il seguente codice alla classe:

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

non saprei dire perché, ma in questo caso il verificatore statica viene visualizzato a prendere in considerazione l'assegnazione campo privato e l'assenza di metodi che modificano è una prova sufficiente che il campo non sarà modificato. Potrebbe essere un bug nel verificatore? Potrebbe valere la pena di segnalare il Code Contracts forum.