False positive with exhaustive switch over enum type

[msridhar]

Test:

class Foo {
    enum Type { TYPE1, TYPE2 }
    static void test(Type type) {
        String t = null;
        switch (type) {
            case TYPE1:
                t = "hello";
                break;
            case TYPE2:
                t = "goodbye";
        }
        t.hashCode();
    }
}

With Checker Framework 3.43.0 the Nullness Checker reports an error:

Foo.java:14: error: [dereference.of.nullable] dereference of possibly-null reference t
        t.hashCode();
        ^
1 error

This is a false positive, and no such error is reported with Checker Framework 3.42.0. Sorry, not set up to test the master branch on this machine, but I'll try that soon.

NullAway also reports a false positive after updating to the 3.43.0 version of dataflow, so I expect this is some new imprecision in the control-flow graph.

[msridhar]

This bisected to 921a66e, i.e., eisop#620. Upon further thought, this may be a true positive report. The code does not even compile if you rewrite it to not use an initializer expression:

class Foo {
    enum Type { TYPE1, TYPE2 }
    static void test(Type type) {
        String t;
        switch (type) {
            case TYPE1:
                t = "hello";
                break;
            case TYPE2:
                t = "goodbye";
        }
        t.hashCode(); // compiler error here that t might not have been initialized
    }
}

The version with a switch expression does compile:

class Foo {
    enum Type { TYPE1, TYPE2 }
    static void test(Type type) {
        String t = switch (type) {
            case TYPE1 -> "hello";
            case TYPE2 -> "goodbye";
        };
        t.hashCode();
    }
}

But for the switch expression, the compiler generates a default case that throws an exception if the enum evolves so that there is a new unmatched case. So, for the original test, it seems reasonable to treat t.hashCode() as possibly being a null dereference.

I'm going to go ahead and close this for now, but I'll reopen if I see a new angle.