Code Contracts warn of "ensures unproven" when locks are involved
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 aa warning: Ensures unproven: this.o1 != null
If I do any of:
o2
in the lock
to o1
, o1
inside the lock
block to o2
, lock
block assigning a new
object
to o2
lock (this.o2)
to if (this.o2 != null)
, 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:
lock
in the real code)? 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.
Add the following code to your class:
[ContractInvariantMethod]
private void ObjectInvariants()
{
Contract.Invariant(o1 != null);
}
I couldn't tell you why, but in this case the static verifier does appear to consider private field assignment and an absence of methods that modify it as sufficient evidence that the field will not be modified. It could be a bug in the verifier? Might be worth reporting on the Code Contracts forum.
链接地址: http://www.djcxy.com/p/12908.html上一篇: JdbcTemplate多个结果集
下一篇: 代码合同警告“确保未经证实”涉及锁定时