Аннотирование Реентерабельность с Java Checker Framework в Nullness Checker

Question

Я пытаюсь из Nullness шашка Checker Framework «s с 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. Но в моем фактическом использовании я хотел бы сохранить возможность установки поля в null.

Заранее благодарен!

Answer 1

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

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

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

К сожалению, Checker Framework в настоящее время не имеет этой функции. Manual section 21.4.3, "Side effects, determinism, purity, and flow-sensitive analysis", обсуждает, как Checker Framework указывает на чистоту или свободу от побочных эффектов. Аннотации @SideEffectFree и @Pure в настоящее время являются «ничего или ничего».

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