Code Contracts warn of "ensures unproven" when locks are involved

Question

I'm trying to work out 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 Code Contract static analysis tool, it prints a a warning: Ensures unproven: this.o1 != null

If I do any of:

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

the 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 causes the 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:

1. Why is this warning occurring?
2. What can be done to prevent it (bearing in mind this is a toy example and there's actually stuff happening inside the lock in the real code)?

Answer 1

Here's how the static checker treats locks and invariants:

If you lock something with the form lock(x.foo) { ... }, the static checker considers x.foo as the protecting lock of x. At the end of the lock scope, it assume that other threads might access x and modify it. As a result, the static checker assumes that all fields of x only satisfy the object invariant after the lock scope, nothing more.

Note that this is not considering all thread interleavings, just interleavings at end of lock scopes.