Как исправить ошибку Checker Framework java: [contracts.precondition.not.satisfied] незащищенный вызов метода «method()», требующий удержания «Holding.yz»

Как правильно позвонить 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] незащищенный вызов метода 'method()', требующий удержания 'Holding.yz'


java checker-framework
person ieXcept    schedule 16.08.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Похоже, это была ошибка в Checker Framework: он знал, как обрабатывать переменные, объявленные как ReentrantLock, но не как обрабатывать переменные, объявленные как его интерфейс Lock.

Эта ошибка исправлена в файле репозиторий управления версиями Git, но не в текущий выпуск, версия 2.1.1.

Используя версию из Git, ваш код выполняет проверку типов для меня после устранения одной проблемы: ваш метод main должен быть аннотирован как @MayReleaseLocks.

person mernst    schedule 18.08.2016