How to fix Checker Framework Error java: [contracts.precondition.not.satisfied] unguarded call to method 'method()' requiring 'Holding.y.z' to be held

Question

How to properly call method() from 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();
            }
        }
    }
}

Error:(37, 23) java: [contracts.precondition.not.satisfied] unguarded call to method 'method()' requiring 'Holding.y.z' to be held

Answer 1

It looks like this was a bug in the Checker Framework: it knew how to handle variables declared as ReentrantLock, but not how to handle variables declared as its interface Lock.

That bug is fixed in the Git version control repository but not in the current release, version 2.1.1.

Using the version from Git, your code type-checks for me, after fixing one problem: your main method needs to be annotated as @MayReleaseLocks.