Аннотирование повторного входа с помощью Nullness Checker в Java Checker Framework

Я пробую Checker Framework Nullness Checker Framework с Java 8. Когда я запускаю проверку на следующий код:

import java.util.HashMap;
import java.util.Map;

import org.checkerframework.checker.nullness.qual.Nullable;

class A {
    public void f() {}
}

public class Foo {
    private Map<A,Integer> map = new HashMap<>();
    private @Nullable A x;

    public void setX(@Nullable A x) {
        this.x = x;
    }

    public void call() {
        if (x != null) {
            map.put(x, 0);
            x.f();
        }
    }
}

контролер выдает предупреждение на x.f();: разыменование возможной нулевой ссылки x. Это имеет смысл, конечно. Checker Framework не знает, что map.put делает. Возможно, объект карты уже имеет ссылку на this, а затем позвоните setX(null) в теме.

Теперь мой вопрос заключается в следующем. Есть ли способ сообщить Checker Framework, что метод не изменяет какой-либо объект, кроме объекта, к которому он обращен? Так как map.put не вызывает setX метод, поэтому значение x не изменится.

Чтобы избавиться от предупреждения, я мог бы изменить метод вызова на:

public void call() {
    A y = x;
    if (y != null) {
        map.put(y, 0);
        y.f();
    }
}

Теперь нет никаких предупреждений. Это также имеет смысл: локальная переменная не может быть доступна извне. Но я не люблю вводить эту локальную переменную с единственной целью - избавиться от предупреждения.

Кроме того, я мог бы аннотировать поле x от @MonotonicNonNull, Но в моем реальном случае я хотел бы оставить возможность установки поля равным нулю.

Заранее спасибо!

Источник

1 ответ

Решение

Ваш вопрос уже дает несколько отличных способов подавить предупреждение, чтобы вы четко знали, что делаете.

Тем не менее, вы хотите лучше. Вы хотите знать, как заставить Checker Framework никогда не выдавать предупреждение. Ваш ключевой вопрос:

Есть ли способ сообщить Checker Framework, что метод не изменяет какой-либо объект, кроме объекта, к которому он обращен?

К сожалению, Checker Framework в настоящее время не имеет этой функциональности. В разделе 21.4.3 Руководства "Побочные эффекты, детерминизм, чистота и анализ, чувствительный к потоку", обсуждается, как Средство проверки показывает чистоту или отсутствие побочных эффектов. Аннотации @SideEffectFree и @Pure в настоящее время являются "все или ничего".

Ваше предложение аннотаций частичной чистоты было бы полезно: это сделало бы Checker Framework более выразительным и уменьшило бы необходимость подавления предупреждений, как это требуется в настоящее время. (С другой стороны, пользователям будет полезно учиться еще раз; компромисс между сложностью и выразительностью всегда есть.) Я предлагаю вам предложить эту функцию разработчикам Checker Framework.

Источник
Другие вопросы по тегам