我正在尝试使用以下示例来研究.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的所有字段仅满足锁定范围之后的对象不变量,仅此而已.
请注意,这不考虑所有线程交错,只是在锁定范围结束时进行交错.
