0

から適切に呼び出す方法method()はmain(..)?

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] 'Holding.yz' を保持する必要があるメソッド 'method()' への無防備な呼び出し

4

1 に答える 1

1

これは Checker フレームワークのバグだったようです: として宣言された変数を処理する方法は知っていましたReentrantLockが、 interface として宣言された変数を処理する方法を知っていませんでしたLock。

このバグはGit バージョン管理リポジトリで修正されていますが、現在のリリースであるバージョン 2.1.1 では修正されていません。

Git のバージョンを使用すると、1 つの問題を修正した後、コードの型チェックが行われます。mainメソッドには@MayReleaseLocks.

于 2016-08-18T03:14:55.203 に答える