Precondition check on field from superclass

Take the following example:

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;

class Parent {
  protected Integer foo;

  public Parent() {
    initFields();
  }

  @EnsuresNonNull("foo")
  private void initFields(@UnknownInitialization Parent this) {
    foo = 42;
  }
}

class Child extends Parent {
  private String bar;

  public Child() {
    // super constructor implicitly called, foo initialized
    initFields();
  }

  @RequiresNonNull("foo")
  @EnsuresNonNull("bar")
  private void initFields(@UnknownInitialization Child this) {
    bar = String.valueOf(foo);
  }

  private void foom() {
    // assert foo != null : "@AssumeAssertion(nullness)"; // SHOULDN'T BE NECESSARY!
    initFields();
  }
}

Running the Nullness Checker produces:

Parent.java:34: error: [contracts.precondition.not.satisfied] initFields's precondition about 'this.foo' is not satisfied
    initFields();
              ^

Which seems like a false positive: the receiver of method foom is fully initialized, so the pre-condition is established.

I first thought it might have to do with the receiver of initFields being @UnknownInitialization, but the following simpler example type checks without error:

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;

class One {
  private Integer foo;
  private String bar;

  public One() {
    foo = 42;
    initFields();
  }

  @RequiresNonNull("foo")
  @EnsuresNonNull("bar")
  private void initFields(@UnknownInitialization(Object.class) One this) {
    bar = String.valueOf(foo);
  }

  private void foom() {
    initFields();
  }
}

So it seems to be related to the field being from the superclass.

This example is a minimized version of the issue reported in https://groups.google.com/d/msg/checker-framework-discuss/Vauq_jzUFyE/cFBPp6tYCQAJ

Start with the minimized Java examples in the issue and reproduce the Nullness Checker diagnostic for the subclass case. Trace the Nullness Checker’s handling of @RequiresNonNull on a method receiver and inherited fields; done means the valid call in foom no longer reports contracts.precondition.not.satisfied while the simpler example remains valid.