java - 如何修复 Checker Framework 错误 java : [contracts. precondition.not.satisfied] 对方法 'method()' 的无保护调用，需要保留 'Holding.y.z'

Question

如何从main(..)正确调用method()？

class LockCheckerTest {
    static class Y {
        final Lock z = new ReentrantLock(true);
    }

    private final static Date x = new Date((long) (System.currentTimeMillis() * Math.random()));
    private final static Y y = new Y();

    @Holding({"x", "y.z"})
    @ReleasesNoLocks
    static void method() {
        System.out.println(x);
    }

    public static void main(String[] args) {
        synchronized (x) {  // acquire intrinsic lock of 'x' 
            synchronized (y) { // locking 'y' is not required, just trying to compile
                y.z.lock(); // acquire explicit lock 'y.z'
                method();  // ERROR
                y.z.unlock();
            }
        }
    }
}

错误:(37, 23) java: [contracts.precondition.not.satisfied] 对方法“method()”的无保护调用，需要持有“Holding.y.z”

Answer 1

看起来这是 Checker 框架中的一个错误:它知道如何处理声明为 ReentrantLock 的变量，但不是如何处理声明为其接口(interface)的变量 Lock .

该错误是 fixed在 Git version control repository但不在 current release, version 2.1.1 中.

使用 Git 的版本，在修复一个问题后，您的代码会为我进行类型检查:您的 main 方法需要注释为 @MayReleaseLocks .