Strong assignment doesn't update fields

[kelloggm]

Consider the following example from the nullness checker:

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

class ObjectAssignment {

   @Nullable Object o;

   static void test_nullness(ObjectAssignment a, ObjectAssignment b) {
    a.o = new Object();
    b = a;
    int k = b.o.hashCode(); // issues a warning
    int j = a.o.hashCode(); // does not issue a warning
    }
}

This also occurs in other checkers (e.g. Index). In general, if an object a with field f is assigned (i.e. a = b), then a.f should have the same type as b.f.

[kelloggm]

I originally thought this was an Index Checker problem; kelloggm#127 has some examples of the problem's manifestations in the Index Checker.

[smillst]

Here are some similar Index Checker test cases:

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.NonNegative;

public class ArrayAssignmentSameLenTest {

  static class Partial {
    private final int[] iValues;
    Partial(@NonNegative int n) {
      iValues = new int[n];
    }
  }

  private final Partial iBase;
  private final @IndexFor("iBase.iValues") int iFieldIndex;

  ArrayAssignmentSameLenTest(Partial partial, @IndexFor("#1.iValues") int fieldIndex) {
    iBase = partial;
    iFieldIndex = fieldIndex;
  }

}

import org.checkerframework.checker.index.qual.*;

class ObjectAssignment {
    int x;

    static void do_things(ObjectAssignment a, ObjectAssignment b) {
    a.x = 5; // a.x is @Positive
    b = a; // b.x is now a.x, so it's also @Positive
    @Positive int y = b.x; // issues a warning
    @Positive int z = a.x; // does not issue a warning
    }
}