Inline Initialized Fields Are Not Considered Nullable Before Initialization

[GoogleCodeExporter]

The following code will produce a NPE at runtime, but does not cause an error 
in the checker framework:

/*>>>import 
org.checkerframework.checker.initialization.qual.UnderInitialization;*/

class Foo {
  static class Bar {
    Bar() {
      doFoo();
    }

    String doFoo(/*>>>@UnderInitialization Bar this*/) {
      return "";
    }
  }

  static class Baz extends Bar {
    String myString = "hello";

    @Override
    String doFoo(/*>>>@UnderInitialization Baz this*/) {
      return myString.toLowerCase();
    }
  }

  public static void main(String[] args) {
    new Baz();
  }
}

Moving the initialization of myString into an anonymous initializer correctly 
causes the checker to emit an error:

/*>>>import 
org.checkerframework.checker.initialization.qual.UnderInitialization;*/

class Foo {
  static class Bar {
    Bar() {
      doFoo();
    }

    String doFoo(/*>>>@UnderInitialization(Bar.class) Bar this*/) {
      return "";
    }
  }

  static class Baz extends Bar {
    String hello;

    {
      hello = "world";
    }

    @Override
    String doFoo(/*>>>@UnderInitialization(Bar.class) Baz this*/) {
      return hello.toLowerCase();
    }
  }

  public static void main(String[] args) {
    new Baz();
  }
}

Original issue reported on code.google.com by eatnumb...@google.com on 9 Mar 2015 at 8:37

[GoogleCodeExporter]

Ping. Can someone take a look at this?

Original comment by eatnumb...@google.com on 17 Mar 2015 at 12:30

[GoogleCodeExporter]

Thanks for the test case! I can reproduce the issue and am looking into it.

Original comment by wdi...@gmail.com on 17 Mar 2015 at 3:03

• Changed state: Accepted