[dereference.of.nullable] on conditional final field access

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

class CF {

    private final @Nullable Ref ref;

    CF(@Nullable Ref ref) {
        this.ref = ref;
    }

    void fun(CF other) {
        if (this.ref == null && other.ref == null) {
            System.out.println("Both null");
        } else if (this.ref == null) {
            System.out.println(other.ref.fun() + " should not be null");
        } else if (other.ref == null) {
            System.out.println(this.ref.fun() + " should not be null");
        } else {
            System.out.println(this.ref.fun() + " and " + other.ref.fun() + " should not be null");
        }
    }

    static class Ref {
        String fun() { return "fun"; }
    }
}

Running the default NullnessChecker

checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker CF.java

returns the following false-positive

CF.java:[15,36] error: [dereference.of.nullable] dereference of possibly-null reference other.ref

(first else-if). other.ref shouldn't be null at this point because otherwise the first branch would have been taken (the field is final so it can't be re-assigned by any possible side-effects). I tested against checkerframework 3.17.0 and Java 8.

It's not a showstopper, since one can easily re-arrange the if statements to make it work, but I was a little bit suprised when this popped up during our code-analysis.

Start by reproducing the diagnostic with the provided CF.java example using the default NullnessChecker and checker/bin/javac. Trace how the checker handles final nullable field accesses across the conditional branches, then add a regression test showing that other.ref is accepted in the first else-if without weakening nullness checking.