c# – 代码合同在涉及锁定时警告“确保未经证实”

我正在尝试使用以下示例来研究.NET Code Contracts如何与lock关键字进行交互：

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

当我运行代码契约静态分析工具时,它会输出一个警告：确保未经证实：this.o1！= null

如果我做了以下任何一项：

>将锁中的o2更改为o1,
>将锁定块内的o1更改为o2,
>在锁定块内添加第二行,将新对象分配给o2
>将lock(this.o2)更改为if(this.o2！= null),
>完全删除锁定语句.

警告消失了.

但是,将锁定块内的行更改为var temp = new object(); (因此从方法中删除对o1的所有引用)仍会导致警告：

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

所以有两个问题：

>为什么会出现此警告？
>可以做些什么来防止它(请记住这是一个玩具示例,实际代码中的锁内部实际发生了什么)？

解决方法

以下是静态检查器如何处理锁和不变量：

如果用形式锁(x.foo){…}锁定某些东西,静态检查器会将x.foo视为x的保护锁.在锁定范围的最后,它假定其他线程可能访问x并对其进行修改.因此,静态检查器假定x的所有字段仅满足锁定范围之后的对象不变量,仅此而已.

请注意,这不考虑所有线程交错,只是在锁定范围结束时进行交错.