Code contracts warn that "provides unproven" when locks are involved

Question

I am trying to understand how .NET Code Contracts interact with the lock keyword using the following example:

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

When I run the contract code static analysis tool, it prints a warning: Ensures unproven: this.o1 != null

If I do:

• change o2 to lock to o1 ,
• change o1 inside the lock block to o2 ,
• add second line inside lock block assigning new object to o2
• change lock (this.o2) to if (this.o2 != null) ,
• completely remove the lock statement.

warning disappears.

However, changing the line inside the lock block to var temp = new object(); (thus removing all references to o1 from the method) still raises a warning:

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

---

So there are two questions:

• Why does this warning occur?
• What can be done to prevent this (bearing in mind that this is an example of a toy, but in fact, everything happens inside the lock in real code)?

Answer 1

Here's how a static checker considers locks and invariants:

If you block something with a form lock (x.foo) {...}, a static check treats x.foo as a security lock x. At the end of the blocking area, it is assumed that other threads can access x and modify it. As a result, a static check assumes that all fields x satisfy only the invariant of the object after the blocking region, no more.

Note that this does not apply to all thread interleaving, just iterates over at the end of the lock areas.

Answer 2

Add the following code to your class:

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

I could not tell you why, but in this case, the static verifier seems to consider closing the private field and the absence of methods that change it as sufficient evidence that the field will not be changed. Could this be a mistake in the verifier? It might be worth reporting a code contract forum .