チェッカーフレームワークエラーの修正方法java：[contracts.precondition.not.satisfied] 'Holding.y.z'を保持する必要があるメソッド 'method（）'への不当な呼び出し

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：それがどのように見える

Answer 1

を保持する 'Holding.yz' を必要とする方法に[contracts.precondition.not.satisfied]無防備コール 'メソッド（）'これはChecker Frameworkのバグでした。ReentrantLockと宣言された変数を扱う方法は知っていましたが、そのインターフェイスとして宣言された変数を処理する方法はありませんLock。

fixedはGit version control repositoryにありますが、current release, version 2.1.1にはありません。

Gitのバージョンを使用すると、1つの問題を修正した後にコードタイプがチェックされます。mainメソッドには@MayReleaseLocksの注釈を付ける必要があります。