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

我正在尝试使用以下示例来了解.NET代码合同如何与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();
    }
  }
}

当我运行Code Contract静态分析工具时，它会打印Ensures unproven: this.o1 != null警告： Ensures unproven: this.o1 != null

如果我做任何：

将lock的o2更改为o1 ，

将lock块内的o1更改为o2 ，

在lock块内添加第二行，将new object分配给o2

将lock (this.o2)更改为if (this.o2 != null) ，

完全删除lock语句。

警告消失。

但是，将lock块内的行更改为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();
    }
  }

---

所以有两个问题：

为什么会发生此警告？

可以做些什么来防止它（考虑到这是一个玩具的例子，实际的代码中实际上有东西在lock内发生）？

---

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

如果你用表单锁（x.foo）{...}来锁定某个东西，那么静态检查器会认为x.foo是x的保护锁。 在锁范围的末尾，它假定其他线程可以访问x并修改它。 因此，静态检查器假定x的所有字段只满足锁范围后的对象不变量，仅此而已。

请注意，这不是考虑所有线程交织，只是在锁定范围结束时交织。

---

将以下代码添加到您的类中：

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

我无法告诉你为什么，但在这种情况下，静态验证程序似乎确实考虑了私人字段分配以及缺少将其修改为足以证明该字段不会被修改的证据的方法。 这可能是验证器中的错误？ 可能值得在守则合同论坛上报告。

链接地址: http://www.djcxy.com/p/12907.html

上一篇: Code Contracts warn of "ensures unproven" when locks are involved

下一篇: AutoMapper Profiles and Unit Testing