Я пытаюсь из Nullness шашка Checker Framework «s с Java 8. При запуске проверки на следующий код:Аннотирование Реентерабельность с Java Checker Framework в Nullness Checker
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
. Но в моем фактическом использовании я хотел бы сохранить возможность установки поля в null.
Заранее благодарен!
Не эксперт (просто интересно), но, похоже, несколько [доступных маршрутов] (http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#suppressing-warnings -nullness). Я бы, вероятно, пошел с 'assert x! = Null' после' map.put', но это ваш выбор. – OldCurmudgeon