java - Java Checker Framework の Nullness Checker を使用して再入可能性に注釈を付ける

Question

Java 8 でChecker Frameworkの Nullness チェッカーを試しています。次のコードでチェッカーを実行すると:

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変化しません。

警告を取り除くには、call メソッドを次のように変更します。

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

現在、警告はありません。これも理にかなっています。ローカル変数は外部からアクセスできません。しかし、警告を取り除くことだけを目的としてこのローカル変数を導入するのは好きではありません。

または、フィールドxに@MonotonicNonNull. しかし、私の実際の使用例では、フィールドを null に設定できるようにしたいと考えています。

前もって感謝します！