Implicit default in enum switch expressions not counted

[tmarback]

When using a switch expression that covers all values of an enum but does not have a default case, it seems that Checker does not account for the implicit default case added by the compiler and thinks that the resulting value may be uninitialized:

enum Bar { VAL1, VAL2, VAL3 }
class Foo {
    public String foo( Bar b ) {
        final var s = switch ( b ) {
            case VAL1 -> "1";
            case VAL2 -> "2";
            case VAL3 -> "3";
        };
        return s;
    }
}

> .\bin\javac.bat -cp . -processor nullness Foo.java
Foo.java:10: error: [return] incompatible types in return.
        return s;
               ^
  type of expression: @UnknownInitialization @Nullable String
  method return type: @Initialized @NonNull String
1 error

If I add a default case, the error goes away:

enum Bar { VAL1, VAL2, VAL3 }
class Foo {
    public String foo( Bar b ) {
        final var s = switch ( b ) {
            case VAL1 -> "1";
            case VAL2 -> "2";
            case VAL3 -> "3";
            default -> throw new RuntimeException();
        };
        return s;
    }
}

Not having this explicit default should be allowed, as per the spec this is preferrable:

In practice this normally means that a default clause is required; however, in the case of an enum switch expression that covers all known constants, a default clause is inserted by the compiler to indicate that the enum definition has changed between compile-time and runtime. Relying on this implicit default clause insertion makes for more robust code; now when code is recompiled, the compiler checks that all cases are explicitly handled.

Funnily enough, this isn't a problem when using the switch statement directly on return:

enum Bar { VAL1, VAL2, VAL3 }
class Foo {
    // No error
    public String foo( Bar b ) {
        return switch ( b ) {
            case VAL1 -> "1";
            case VAL2 -> "2";
            case VAL3 -> "3";
        };
    }
}

All of the examples were ran using the command .\bin\javac.bat -cp . -processor nullness Foo.java, with the code being placed in the Foo.java file, and with the current directory being the root directory of the Checker 3.27.0 release artifact.